src/Provers/classical.ML
changeset 26425 6561665c5cb1
parent 26412 0918f5c0bbca
child 26470 e44d24620515
     1.1 --- a/src/Provers/classical.ML	Thu Mar 27 14:41:09 2008 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Mar 27 14:41:10 2008 +0100
     1.3 @@ -879,12 +879,12 @@
     1.4    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
     1.5  
     1.6  val change_claset_of = change o #1 o GlobalClaset.get;
     1.7 -fun change_claset f = change_claset_of (ML_Context.the_context ()) f;
     1.8 +fun change_claset f = change_claset_of (ML_Context.the_global_context ()) f;
     1.9  
    1.10  fun claset_of thy =
    1.11    let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
    1.12    in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
    1.13 -val claset = claset_of o ML_Context.the_context;
    1.14 +val claset = claset_of o ML_Context.the_global_context;
    1.15  
    1.16  fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
    1.17  fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;