--- a/QuotMain.thy	Thu Nov 12 02:18:36 2009 +0100
+++ b/QuotMain.thy	Thu Nov 12 02:54:40 2009 +0100
@@ -1032,7 +1032,9 @@
   let
     fun matches (ty1, ty2) =
       Type.raw_instance (ty1, Logic.varifyT ty2);
-    val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+    val qty_name = fst (dest_Type qty)
+    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)
     val rel = #rel quotdata