--- 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