--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Apr 25 15:13:33 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Apr 25 15:52:03 2010 +0200
@@ -99,7 +99,7 @@
|> (fn ctxt1 => ctxt1
|> prepare
|-> (fn us => fn ctxt2 => ctxt2
- |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
+ |> Proof.theorem NONE (fn thmss => fn ctxt =>
let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
end
@@ -188,7 +188,7 @@
fun prove thy meth vc =
ProofContext.init thy
- |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
+ |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
|> Proof.apply meth
|> Seq.hd
|> Proof.global_done_proof