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.
Quot/quotient_tacs.ML
changeset 776 d1064fa29424
parent 775 26fefde1d124
child 781 f3a24012e9d8 
--- a/Quot/quotient_tacs.ML	Tue Dec 22 21:16:11 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 21:31:44 2009 +0100
@@ -586,11 +586,9 @@
   val thy = ProofContext.theory_of ctxt
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
-  val reg_goal = 
-        Syntax.check_term ctxt (regularize_trm ctxt (rtrm', qtrm'))
+  val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
         handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
-  val inj_goal = 
-        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
+  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
         handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
 in
   Drule.instantiate' []
nominal2