--- a/Quot/quotient_def.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_def.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -3,6 +3,7 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
+  
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
@@ -29,10 +30,13 @@
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
 fun get_fun_aux lthy s fs =
-  case (maps_lookup (ProofContext.theory_of lthy) s) of
-    SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-  | NONE      => raise
-        (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
+let
+  val thy = ProofContext.theory_of lthy
+  val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])
+  val info = maps_lookup thy s handle NotFound => raise exc
+in
+  list_comb (Const (#mapfun info, dummyT), fs)
+end
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)
@@ -72,9 +76,9 @@
   | (TFree x, TFree x') =>
      if x = x'
      then mk_identity qty
-     else raise (LIFT_MATCH "get_fun")
-  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
-  | _ => raise (LIFT_MATCH "get_fun")
+     else raise (LIFT_MATCH "get_fun (frees)")
+  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)")
+  | _ => raise (LIFT_MATCH "get_fun (default)")
 
 (* interface and syntax setup *)
 
@@ -84,6 +88,7 @@
 (* - name and attributes of the meta eq           *)
 (* - the new constant including its type          *)
 (* - the rhs of the definition                    *)
+
 fun quotient_def mx attr lhs rhs lthy =
 let
   val Free (lhs_str, lhs_ty) = lhs;
@@ -115,9 +120,9 @@
 
 val quotdef_parser =
   (SpecParse.opt_thm_name ":" --
-  OuterParse.term) --
-  (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
-  OuterParse.term)
+     OuterParse.term) --
+      (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
+         OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)