changeset 60822 | 4f58f3662e7d |
parent 60651 | 1049f3724ac0 |
child 63636 | 6f38b7abb648 |
--- a/src/HOL/Tools/simpdata.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/HOL/Tools/simpdata.ML Tue Jul 28 20:59:39 2015 +0200 @@ -112,8 +112,7 @@ end; in atoms end; -fun mksimps pairs ctxt = - map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt); +fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt; fun unsafe_solver_tac ctxt = let