# HG changeset patch
# User bulwahn
# Date 1319716255 -7200
# Node ID 728ed9d28c63bd7075af497521f286d3abf84797
# Parent  5995ab88a00fa87a7bd349d8115fb449f8c45a0b
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

diff -r 5995ab88a00f -r 728ed9d28c63 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:54 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:55 2011 +0200
@@ -12,8 +12,7 @@
 
   type maps_info = {mapfun: string, relmap: string}
   val maps_defined: theory -> string -> bool
-  (* FIXME functions called "lookup" must return option, not raise exception! *)
-  val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
+  val maps_lookup: theory -> string -> maps_info option
   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
@@ -28,6 +27,7 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val transform_qconsts: morphism -> qconsts_info -> qconsts_info
+  (* FIXME functions called "lookup" must return option, not raise exception! *)
   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
@@ -67,13 +67,9 @@
   fun merge data = Symtab.merge (K true) data
 )
 
-fun maps_defined thy s =
-  Symtab.defined (MapsData.get thy) s
+fun maps_defined thy s = Symtab.defined (MapsData.get thy) s
 
-fun maps_lookup thy s =
-  (case Symtab.lookup (MapsData.get thy) s of
-    SOME map_fun => map_fun
-  | NONE => raise NotFound)
+fun maps_lookup thy s = Symtab.lookup (MapsData.get thy) s
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo)  (* FIXME *)
diff -r 5995ab88a00f -r 728ed9d28c63 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:54 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:55 2011 +0200
@@ -63,13 +63,9 @@
   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
 
 fun get_mapfun ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
-      raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-  in
-    Const (mapfun, dummyT)
-  end
+  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
+    SOME map_data => Const (#mapfun map_data, dummyT)
+  | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
 
 (* makes a Free out of a TVar *)
 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
@@ -275,13 +271,9 @@
   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
-      raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
-  in
-    Const (relmap, dummyT)
-  end
+  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
+    SOME map_data => Const (#relmap map_data, dummyT)
+  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
 
 fun mk_relmap ctxt vs rty =
   let