diff -r b66d754bf1c2 -r 1ae5afcddcd4 Attic/Quot/quotient_tacs.ML
--- a/Attic/Quot/quotient_tacs.ML	Mon Mar 15 17:51:35 2010 +0100
+++ b/Attic/Quot/quotient_tacs.ML	Mon Mar 15 17:52:31 2010 +0100
@@ -603,9 +603,9 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
-    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+    handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
-    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+    handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),