1.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Feb 19 11:56:11 2010 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Feb 19 16:11:45 2010 +0100
     1.3 @@ -327,7 +327,7 @@
     1.4  
     1.5       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
     1.6         If the premises get simplified, then the proofs could fail.*)
     1.7 -     val min_ss = Simplifier.theory_context thy empty_ss
     1.8 +     val min_ss = Simplifier.global_context thy empty_ss
     1.9             setmksimps (map mk_eq o ZF_atomize o gen_all)
    1.10             setSolver (mk_solver "minimal"
    1.11                        (fn prems => resolve_tac (triv_rls@prems)