--- a/src/Sequents/simpdata.ML Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Sequents/simpdata.ML Tue Jul 28 20:59:39 2015 +0200
@@ -71,8 +71,7 @@
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
|> Simplifier.set_subgoaler asm_simp_tac
- |> Simplifier.set_mksimps (fn ctxt =>
- map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt))
+ |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt)
|> Simplifier.set_mkcong mk_meta_cong
|> simpset_of;