src/Provers/classical.ML
changeset 22095 07875394618e
parent 21963 416a5338d2bb
child 22360 26ead7ed4f4b
     1.1 --- a/src/Provers/classical.ML	Fri Jan 19 22:08:01 2007 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Jan 19 22:08:02 2007 +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 (Context.the_context ()) f;
     1.8 +fun change_claset f = change_claset_of (ML_Context.the_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 Context.the_context;
    1.14 +val claset = claset_of o ML_Context.the_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;