src/Pure/simplifier.ML
changeset 26425 6561665c5cb1
parent 24509 23ee6b7788c2
child 26435 bdce320cd426
     1.1 --- a/src/Pure/simplifier.ML	Thu Mar 27 14:41:09 2008 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Thu Mar 27 14:41:10 2008 +0100
     1.3 @@ -110,10 +110,10 @@
     1.4  val get_simpset = ! o GlobalSimpset.get;
     1.5  
     1.6  fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f);
     1.7 -fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_context ()) f);
     1.8 +fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f);
     1.9  
    1.10  fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
    1.11 -val simpset = simpset_of o ML_Context.the_context;
    1.12 +val simpset = simpset_of o ML_Context.the_global_context;
    1.13  
    1.14  
    1.15  fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;