--- a/QuotMain.thy	Thu Nov 12 12:07:33 2009 +0100
+++ b/QuotMain.thy	Thu Nov 12 13:56:07 2009 +0100
@@ -1030,10 +1030,8 @@
 ML {*
 fun lookup_quot_data lthy qty =
   let
-    fun matches (ty1, ty2) =
-      Type.raw_instance (ty1, Logic.varifyT ty2);
     val qty_name = fst (dest_Type qty)
-    val SOME quotdata = quotdata_lookup lthy qty_name 
+    val SOME quotdata = quotdata_lookup lthy qty_name
                   (* cu: Changed the lookup\<dots>not sure whether this works *)
     (* TODO: Should no longer be needed *)
     val rty = Logic.unvarifyT (#rtyp quotdata)