--- a/QuotMain.thy	Tue Nov 24 15:18:00 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 16:10:31 2009 +0100
@@ -1180,7 +1180,7 @@
   val qtrm_str = quote (Syntax.string_of_term lthy qtrm)
   val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]
 in
-  raise LIFT_MATCH (space_implode " " msg)
+  raise error (space_implode " " msg)
 end 
 *}
 

--- a/quotient.ML	Tue Nov 24 15:18:00 2009 +0100
+++ b/quotient.ML	Tue Nov 24 16:10:31 2009 +0100
@@ -1,7 +1,5 @@
 signature QUOTIENT =
 sig
-  exception LIFT_MATCH of string 
-
   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
 
@@ -11,9 +9,6 @@
 structure Quotient: QUOTIENT =
 struct
 
-(* exception for when quotient and lifted things do not match *)
-exception LIFT_MATCH of string 
-
 (* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let

--- a/quotient_def.ML	Tue Nov 24 15:18:00 2009 +0100
+++ b/quotient_def.ML	Tue Nov 24 16:10:31 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 *)