diff -r 970e86082cd7 -r e3732ed89dfc Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Jan 08 10:39:08 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Jan 08 10:44:30 2010 +0100
@@ -158,7 +158,7 @@
   val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
   val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp id_simps}
                        addsimprocs [simproc] 
                        addSolver equiv_solver addSolver quotient_solver
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)