diff -r b4ffb8826105 -r 26fefde1d124 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Dec 22 21:06:46 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 21:16:11 2009 +0100
@@ -14,7 +14,6 @@
 open Quotient_Info;
 open Quotient_Term;
 
-
 (* Since HOL_basic_ss is too "big" for us, we *)
 (* need to set up our own minimal simpset.    *)
 fun  mk_minimal_ss ctxt =
@@ -588,7 +587,7 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = 
-        Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
+        Syntax.check_term ctxt (regularize_trm 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'))