# HG changeset patch
# User boehmes
# Date 1269248062 -3600
# Node ID d82c0dd51794099c50e48d1b24bc402ce0adec3f
# Parent  d4218a55cf209c108a6676aeb945c7658e492c97
use a proof context instead of a local theory

diff -r d4218a55cf20 -r d82c0dd51794 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 22 09:46:04 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 22 09:54:22 2010 +0100
@@ -63,9 +63,8 @@
       THEN' Boogie_Tactics.drop_assert_at_tac
       THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
 in
-fun boogie_vc (vc_name, vc_opts) lthy =
+fun boogie_vc (vc_name, vc_opts) thy =
   let
-    val thy = ProofContext.theory_of lthy
     val vc = get_vc thy vc_name
 
     fun extract vc l =
@@ -92,16 +91,16 @@
       | _ => (pair ts, K I))
 
     val discharge = fold (Boogie_VCs.discharge o pair vc_name)
-    fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
+    fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
       | after_qed _ = I
   in
-    lthy
+    ProofContext.init thy
     |> fold Variable.auto_fixes ts
-    |> (fn lthy1 => lthy1
+    |> (fn ctxt1 => ctxt1
     |> prepare
-    |-> (fn us => fn lthy2 => lthy2
+    |-> (fn us => fn ctxt2 => ctxt2
     |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
-         let val export = map (finish lthy1) o ProofContext.export ctxt lthy2
+         let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
          in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
   end
 end
@@ -300,7 +299,7 @@
     "Enter into proof mode for a specific verification condition."
     OuterKeyword.thy_goal
     (vc_name -- vc_opts >> (fn args =>
-      (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args))))
+      (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
 
 
 val quick_timeout = 5