--- a/Quot/quotient_info.ML	Mon Jan 11 11:51:19 2010 +0100
+++ b/Quot/quotient_info.ML	Mon Jan 11 15:13:09 2010 +0100
@@ -12,7 +12,6 @@
   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   val transform_quotdata: morphism -> quotdata_info -> quotdata_info
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
-  val quotdata_lookup_type: theory -> typ -> quotdata_info   (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
   val print_quotinfo: Proof.context -> unit
@@ -159,16 +158,6 @@
 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
 
-fun quotdata_lookup_type thy qty =
-  let
-    val smt = Symtab.dest (QuotData.get thy);
-    fun matches (_, x) = Sign.typ_instance thy (qty, (#qtyp x))
-  in
-    case (find_first matches smt) of
-      SOME (_, x) => x
-    | _ => raise NotFound
-  end
-
 fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = 

--- a/Quot/quotient_term.ML	Mon Jan 11 11:51:19 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Jan 11 15:13:09 2010 +0100
@@ -413,21 +413,24 @@
   | (_, Const _) =>
        let
          val thy = ProofContext.theory_of ctxt
-         fun matches_typ T T' = (
-           let
-             val rty = #rtyp (quotdata_lookup_type thy T')
-           in
-             if Sign.typ_instance thy (T, rty) then true else T = T'
-           end
-           handle Not_found => (* raised by quotdata_lookup_type *)
-             case (T, T') of
-               (TFree _, TFree _) => true
-             | (TVar _, TVar _) => true
-             | (Type (s, tys), Type (s', tys')) =>
-                 (* '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
-         )
+         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'
            | same_const _ _ = false
        in