--- a/src/ZF/Tools/inductive_package.ML Thu Nov 24 20:45:34 2011 +0100
+++ b/src/ZF/Tools/inductive_package.ML Thu Nov 24 21:01:06 2011 +0100
@@ -326,8 +326,9 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
- val min_ss = Simplifier.global_context thy empty_ss
- setmksimps (K (map mk_eq o ZF_atomize o gen_all))
+ val min_ss =
+ (Simplifier.global_context thy empty_ss
+ |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
setSolver (mk_solver "minimal"
(fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
ORELSE' assume_tac