--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Sun Nov 14 23:55:25 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Mon Nov 15 00:20:36 2010 +0100
@@ -6,6 +6,7 @@
theory Boogie_Dijkstra
imports Boogie
+uses ("Boogie_Dijkstra.b2i")
begin
text {*
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Sun Nov 14 23:55:25 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Mon Nov 15 00:20:36 2010 +0100
@@ -6,6 +6,7 @@
theory Boogie_Max
imports Boogie
+uses ("Boogie_Max.b2i")
begin
text {*
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Sun Nov 14 23:55:25 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Mon Nov 15 00:20:36 2010 +0100
@@ -6,6 +6,7 @@
theory Boogie_Max_Stepwise
imports Boogie
+uses ("Boogie_Max.b2i")
begin
text {*
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Sun Nov 14 23:55:25 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Mon Nov 15 00:20:36 2010 +0100
@@ -6,6 +6,7 @@
theory VCC_Max
imports Boogie
+uses ("VCC_Max.b2i")
begin
text {*
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Nov 14 23:55:25 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 15 00:20:36 2010 +0100
@@ -19,16 +19,16 @@
val ext = "b2i"
fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
val base_path = add_ext (Path.explode base_name)
- val path_id = Thy_Load.check_file [Thy_Load.master_directory thy] base_path
+ val (full_path, _) =
+ Thy_Load.check_file [Thy_Load.master_directory thy] base_path
val _ = Boogie_VCs.is_closed thy orelse
error ("Found the beginning of a new Boogie environment, " ^
"but another Boogie environment is still open.")
in
thy
- |> Thy_Load.require base_path
- |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id)
- |> Thy_Load.provide (base_path, path_id)
+ |> Boogie_Loader.load_b2i (not quiet) offsets full_path
+ |> Thy_Load.provide_file base_path
end