src/HOL/Tools/choice_specification.ML

--- a/src/HOL/Tools/choice_specification.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Mon May 03 14:25:56 2010 +0200
@@ -225,7 +225,7 @@
         #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
       thy
-      |> ProofContext.init
+      |> ProofContext.init_global
       |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;