Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Attic/Quot/quotient_tacs.ML
changeset 1450 1ae5afcddcd4
parent 1438 61671de8a545 
--- 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'),
nominal2