diff -r 98dbe4fe6afe -r 980fdf92a834 quotient_def.ML
--- a/quotient_def.ML	Tue Nov 24 19:09:29 2009 +0100
+++ b/quotient_def.ML	Wed Nov 25 03:45:44 2009 +0100
@@ -31,30 +31,11 @@
 
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-fun ty_strs lthy (ty1, ty2) = 
-  (quote (Syntax.string_of_typ lthy ty1),
-   quote (Syntax.string_of_typ lthy ty2))
-
-fun ty_lift_error1 lthy rty qty =
-let
-  val (rty_str, qty_str) = ty_strs lthy (rty, qty) 
-  val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."]
-in
-  error (space_implode " " msg)
-end
-
-fun ty_lift_error2 lthy rty qty =
-let
-  val (rty_str, qty_str) = ty_strs lthy (rty, qty)   
-  val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."]
-in
-  error (space_implode " " msg)
-end
-
 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      => error (space_implode " " ["No map function for type", quote s, "."])
+  | NONE      => raise 
+        (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)
@@ -93,9 +74,9 @@
   | (TFree x, TFree x') =>
      if x = x'
      then mk_identity qty 
-     else ty_lift_error1 lthy rty qty
-  | (TVar _, TVar _) => ty_lift_error2 lthy rty qty
-  | _ => ty_lift_error1 lthy rty qty
+     else raise (LIFT_MATCH "get_fun")
+  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
+  | _ => raise (LIFT_MATCH "get_fun")
 
 fun make_def qconst_bname qty mx attr rhs lthy =
 let