src/Provers/classical.ML
changeset 42361 23f352990944
parent 41581 72a02e3dec7e
child 42439 9efdd0af15ac
     1.1 --- a/src/Provers/classical.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4  fun dup_elim th =
     1.5    let
     1.6      val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
     1.7 -    val ctxt = ProofContext.init_global (Thm.theory_of_thm rl);
     1.8 +    val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
     1.9    in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
    1.10  
    1.11  
    1.12 @@ -850,13 +850,13 @@
    1.13  val get_global_claset = #1 o GlobalClaset.get;
    1.14  val map_global_claset = GlobalClaset.map o apfst;
    1.15  
    1.16 -val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    1.17 +val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
    1.18  fun map_context_cs f = GlobalClaset.map (apsnd
    1.19    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
    1.20  
    1.21  fun global_claset_of thy =
    1.22    let val (cs, ctxt_cs) = GlobalClaset.get thy
    1.23 -  in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
    1.24 +  in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
    1.25  
    1.26  
    1.27  (* context dependent components *)