src/Provers/classical.ML
changeset 36610 bafd82950e24
parent 36546 a9873318fe30
child 36960 01594f816e3a
     1.1 --- a/src/Provers/classical.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon May 03 14:25:56 2010 +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 (Thm.theory_of_thm rl);
     1.8 +    val ctxt = ProofContext.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 @@ -856,7 +856,7 @@
    1.13  
    1.14  fun global_claset_of thy =
    1.15    let val (cs, ctxt_cs) = GlobalClaset.get thy
    1.16 -  in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
    1.17 +  in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
    1.18  
    1.19  
    1.20  (* context dependent components *)