--- a/src/ZF/Tools/inductive_package.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Jan 12 16:37:58 2002 +0100
@@ -341,7 +341,7 @@
(*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 = empty_ss
- setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
+ setmksimps (map mk_eq o ZF_atomize o gen_all)
setSolver (mk_solver "minimal"
(fn prems => resolve_tac (triv_rls@prems)
ORELSE' assume_tac