src/HOL/Tools/Quotient/quotient_term.ML
changeset 45273 728ed9d28c63
parent 45272 5995ab88a00f
child 45274 252cd58847e0
--- 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