--- a/src/Provers/classical.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/Provers/classical.ML Mon May 03 14:25:56 2010 +0200
@@ -210,7 +210,7 @@
fun dup_elim th =
let
val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
- val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+ val ctxt = ProofContext.init_global (Thm.theory_of_thm rl);
in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
@@ -856,7 +856,7 @@
fun global_claset_of thy =
let val (cs, ctxt_cs) = GlobalClaset.get thy
- in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
+ in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
(* context dependent components *)