--- a/QuotMain.thy	Mon Nov 02 09:47:49 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 11:15:26 2009 +0100
@@ -416,8 +416,11 @@
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}
 ML {*
+fun matches (ty1, ty2) =
+  Type.raw_instance (ty1, Logic.varifyT ty2);
+
 fun tyRel ty rty rel lthy =
-  if ty = rty 
+  if matches (rty, ty)
   then rel
   else (case ty of
           Type (s, tys) =>
@@ -892,8 +895,8 @@
 ML {*
 fun lookup_quot_data lthy qty =
   let
-    val SOME quotdata = find_first (fn x => #qtyp x = qty) (quotdata_lookup lthy)
-    val rty = #rtyp quotdata
+    val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+    val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
     val rel_eqv = #equiv_thm quotdata
     val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]