--- a/quotient_info.ML	Thu Nov 19 14:17:10 2009 +0100
+++ b/quotient_info.ML	Fri Nov 20 13:03:01 2009 +0100
@@ -79,7 +79,9 @@
    val extend = I
    val merge = Symtab.merge (K true)) 
 
-val quotdata_lookup_thy = Symtab.lookup o QuotData.get
+fun quotdata_lookup_thy thy str = 
+    Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
+
 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =