diff -r 82cfedb16a99 -r ba057402ea53 quotient_def.ML
--- a/quotient_def.ML	Tue Nov 24 15:15:33 2009 +0100
+++ b/quotient_def.ML	Tue Nov 24 15:31:29 2009 +0100
@@ -40,7 +40,7 @@
   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
-  raise LIFT_MATCH (space_implode " " msg)
+  error (space_implode " " msg)
 end
 
 fun ty_lift_error2 lthy rty qty =
@@ -48,13 +48,13 @@
   val (rty_str, qty_str) = ty_strs lthy (rty, qty)   
   val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."]
 in
-  raise LIFT_MATCH (space_implode " " msg)
+  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      => raise LIFT_MATCH (space_implode " " ["No map function for type", quote s, "."])
+  | NONE      => error (space_implode " " ["No map function for type", quote s, "."])
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)