diff -r 8a1f4227dff9 -r f178958d3d81 quotient_info.ML
--- a/quotient_info.ML	Fri Dec 04 18:32:19 2009 +0100
+++ b/quotient_info.ML	Fri Dec 04 21:42:55 2009 +0100
@@ -1,5 +1,7 @@
 signature QUOTIENT_INFO =
 sig
+  exception NotFound
+
   type maps_info = {mapfun: string, relfun: string}
   val maps_lookup: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
@@ -15,7 +17,7 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
-  val qconsts_lookup: theory -> string -> qconsts_info option
+  val qconsts_lookup: theory -> string -> qconsts_info
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: theory -> qconsts_info list
@@ -29,6 +31,7 @@
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
+exception NotFound
 
 (* data containers *)
 (*******************)
@@ -134,7 +137,10 @@
      rconst = Morphism.term phi rconst,
      def = Morphism.thm phi def}
 
-val qconsts_lookup = Symtab.lookup o QConstsData.get
+fun qconsts_lookup thy str = 
+  case Symtab.lookup (QConstsData.get thy) str of
+    SOME info => info
+  | NONE => raise NotFound
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I