diff -r ab8a58973861 -r cc951743c5e2 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Jan 14 12:23:59 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Jan 14 15:25:24 2010 +0100
@@ -11,6 +11,7 @@
 
   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   val transform_quotdata: morphism -> quotdata_info -> quotdata_info
+  val quotdata_lookup_raw: theory -> string -> quotdata_info option
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
@@ -147,7 +148,9 @@
      equiv_rel = Morphism.term phi equiv_rel,
      equiv_thm = Morphism.thm phi equiv_thm}
 
-fun quotdata_lookup thy str = 
+fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
+
+fun quotdata_lookup thy str =
   case Symtab.lookup (QuotData.get thy) str of
     SOME qinfo => qinfo
   | NONE => raise NotFound