diff -r da8817d01e7c -r 23f352990944 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/Provers/classical.ML	Sat Apr 16 16:15:37 2011 +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_global (Thm.theory_of_thm rl);
+    val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
   in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
 
 
@@ -850,13 +850,13 @@
 val get_global_claset = #1 o GlobalClaset.get;
 val map_global_claset = GlobalClaset.map o apfst;
 
-val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
+val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
 fun map_context_cs f = GlobalClaset.map (apsnd
   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
 
 fun global_claset_of thy =
   let val (cs, ctxt_cs) = GlobalClaset.get thy
-  in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
+  in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
 
 
 (* context dependent components *)