diff -r 26fefde1d124 -r d1064fa29424 Quot/quotient_tacs.ML
--- 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' []