--- a/QuotMain.thy	Tue Nov 24 15:15:33 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 15:31:29 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 
 *}