src/HOL/Boogie/Tools/boogie_commands.ML

     ProofContext.init thy
     |> fold Variable.auto_fixes ts
     |> (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
 end
 

         in par_map f [vc1, vc2] end
     end
 
   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
 in
 fun boogie_narrow_vc (quick, timeout) vc_name meth thy =