diff -r 119f7d6a3556 -r c1989de100b4 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_info.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -3,7 +3,7 @@
   exception NotFound
 
   type maps_info = {mapfun: string, relfun: string}
-  val maps_lookup: theory -> string -> maps_info option
+  val maps_lookup: theory -> string -> maps_info       (* raises NotFound *)
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
   val print_mapsinfo: Proof.context -> unit
@@ -18,7 +18,7 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
-  val qconsts_lookup: theory -> term -> qconsts_info
+  val qconsts_lookup: theory -> term -> qconsts_info    (* raises NotFound *)
   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
@@ -50,7 +50,10 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
-val maps_lookup = Symtab.lookup o MapsData.get
+fun maps_lookup thy s = 
+  case (Symtab.lookup (MapsData.get thy) s) of
+    SOME map_fun => map_fun
+  | NONE => raise NotFound
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
@@ -188,14 +191,15 @@
     | _ => raise NotFound
   end
 
-(* We omit printing the definition *)
 fun print_qconstinfo ctxt =
 let
   fun prt_qconst {qconst, rconst, def} =
       Pretty.block (separate (Pretty.brk 1)
           [Syntax.pretty_term ctxt qconst,
            Pretty.str ":=",
-           Syntax.pretty_term ctxt rconst])
+           Syntax.pretty_term ctxt rconst,
+           Pretty.str "as",
+           Syntax.pretty_term ctxt (prop_of def)])
 in
   QConstsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest