# HG changeset patch
# User boehmes
# Date 1289776836 -3600
# Node ID 293f9f211be0268bf8918f573984030ba18e612f
# Parent  b6f1da38fa24b94147b095f513b1a0be3c657d5a
formal dependency on b2i files

diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- 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 {*
diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/Boogie_Max.thy
--- 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 {*
diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- 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 {*
diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/VCC_Max.thy
--- 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 {*
diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Tools/boogie_commands.ML
--- 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