diff -r c4001cda9da3 -r aaeb5a34d21a Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Feb 12 16:04:10 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Feb 12 16:06:09 2010 +0100
@@ -153,6 +153,7 @@
 
   finally jump back to 1
 *)
+
 fun regularize_tac ctxt =
 let
   val thy = ProofContext.theory_of ctxt
@@ -163,7 +164,8 @@
                        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
                        addsimprocs [simproc]
                        addSolver equiv_solver addSolver quotient_solver
-  val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
+  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
+  val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
 in
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST'