1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 22 09:46:04 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 22 09:54:22 2010 +0100
     1.3 @@ -63,9 +63,8 @@
     1.4        THEN' Boogie_Tactics.drop_assert_at_tac
     1.5        THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
     1.6  in
     1.7 -fun boogie_vc (vc_name, vc_opts) lthy =
     1.8 +fun boogie_vc (vc_name, vc_opts) thy =
     1.9    let
    1.10 -    val thy = ProofContext.theory_of lthy
    1.11      val vc = get_vc thy vc_name
    1.12  
    1.13      fun extract vc l =
    1.14 @@ -92,16 +91,16 @@
    1.15        | _ => (pair ts, K I))
    1.16  
    1.17      val discharge = fold (Boogie_VCs.discharge o pair vc_name)
    1.18 -    fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
    1.19 +    fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
    1.20        | after_qed _ = I
    1.21    in
    1.22 -    lthy
    1.23 +    ProofContext.init thy
    1.24      |> fold Variable.auto_fixes ts
    1.25 -    |> (fn lthy1 => lthy1
    1.26 +    |> (fn ctxt1 => ctxt1
    1.27      |> prepare
    1.28 -    |-> (fn us => fn lthy2 => lthy2
    1.29 +    |-> (fn us => fn ctxt2 => ctxt2
    1.30      |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
    1.31 -         let val export = map (finish lthy1) o ProofContext.export ctxt lthy2
    1.32 +         let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
    1.33           in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
    1.34    end
    1.35  end
    1.36 @@ -300,7 +299,7 @@
    1.37      "Enter into proof mode for a specific verification condition."
    1.38      OuterKeyword.thy_goal
    1.39      (vc_name -- vc_opts >> (fn args =>
    1.40 -      (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args))))
    1.41 +      (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
    1.42  
    1.43  
    1.44  val quick_timeout = 5