src/Provers/classical.ML
changeset 21516 c2a116a2c4fd
parent 20956 00fe22000c6a
child 21646 c07b5b0e8492
     1.1 --- a/src/Provers/classical.ML	Fri Nov 24 17:23:15 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Nov 24 22:05:12 2006 +0100
     1.3 @@ -888,7 +888,7 @@
     1.4  
     1.5  fun claset_of thy =
     1.6    let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
     1.7 -  in context_cs (Context.init_proof thy) (! cs_ref) (ctxt_cs) end;
     1.8 +  in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
     1.9  val claset = claset_of o Context.the_context;
    1.10  
    1.11  fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;