src/HOL/Boogie/Tools/boogie_commands.ML

--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 03 14:25:56 2010 +0200
@@ -94,7 +94,7 @@
     fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
       | after_qed _ = I
   in
-    ProofContext.init thy
+    ProofContext.init_global thy
     |> fold Variable.auto_fixes ts
     |> (fn ctxt1 => ctxt1
     |> prepare
@@ -187,7 +187,7 @@
     end
 
   fun prove thy meth vc =
-    ProofContext.init thy
+    ProofContext.init_global thy
     |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
     |> Proof.apply meth
     |> Seq.hd