--- a/Quot/QuotProd.thy	Wed Jan 13 16:39:20 2010 +0100
+++ b/Quot/QuotProd.thy	Wed Jan 13 16:46:25 2010 +0100
@@ -53,8 +53,6 @@
 
 
 
-(* TODO: Is the quotient assumption q1 necessary? *)
-(* TODO: Aren't there hard to use later? *)
 lemma fst_rsp:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"

--- a/Quot/quotient_term.ML	Wed Jan 13 16:39:20 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 13 16:46:25 2010 +0100
@@ -387,6 +387,27 @@
 (* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)
 
+(* Checks that two types match, for example:
+     rty -> rty   matches   qty -> qty *)
+fun matches_typ thy T T' =
+  case (T, T') of
+    (TFree _, TFree _) => true
+  | (TVar _, TVar _) => true
+  | (Type (s, tys), Type (s', tys')) => (
+      if T = T' then true else
+      let
+        val rty = #rtyp (Quotient_Info.quotdata_lookup thy s')
+      in
+        if Sign.typ_instance thy (T, rty) then true else false
+      end
+      handle Not_found =>
+        if length tys <> length tys' then false else
+        (* 'andalso' is buildin syntax so it needs to be expanded *)
+        fold (fn x => fn y => x andalso y) (map2 (matches_typ thy) tys tys') (s = s')
+      )
+  | _ => false
+
+
 (* produces a regularized version of rtrm
 
    - the result might contain dummyTs           
@@ -437,25 +458,7 @@
   | (_, Const _) =>
        let
          val thy = ProofContext.theory_of ctxt
-         fun matches_typ T T' =
-           case (T, T') of
-             (TFree _, TFree _) => true
-           | (TVar _, TVar _) => true
-           | (Type (s, tys), Type (s', tys')) => (
-               (s = s' andalso tys = tys') orelse
-               (* 'andalso' is buildin syntax so it needs to be expanded *)
-               (fold (fn x => fn y => x andalso y) (map2 matches_typ tys tys') (s = s')
-                handle UnequalLengths => false
-               ) orelse
-               let
-                 val rty = #rtyp (Quotient_Info.quotdata_lookup thy s')
-               in
-                 Sign.typ_instance thy (T, rty)
-               end
-               handle Not_found => false (* raised by quotdata_lookup *)
-             )
-           | _ => false
-         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ T T'
+         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
            | same_const _ _ = false
        in
          if same_const rtrm qtrm then rtrm