diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -220,11 +220,11 @@
                     |> process_all (zip3 alt_names rew_imps frees)
             end
 
-      fun after_qed [[thm]] = ProofContext.background_theory (fn thy =>
+      fun after_qed [[thm]] = Proof_Context.background_theory (fn thy =>
         #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
       thy
-      |> ProofContext.init_global
+      |> Proof_Context.init_global
       |> Variable.declare_term ex_prop
       |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;