# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262958210 -3600
# Node ID e1f1114ae8bd0740d36277d50555e27e3ac8bbfd
# Parent  dd26fbdee924711fff3348df626261a15fe7926f
id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.

diff -r dd26fbdee924 -r e1f1114ae8bd Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Jan 08 11:20:12 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Jan 08 14:43: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 id_simps}
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get ctxt)
                        addsimprocs [simproc] 
                        addSolver equiv_solver addSolver quotient_solver
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)