src/HOL/Boogie/Tools/boogie_commands.ML
changeset 40540 293f9f211be0
parent 40514 db5f14910dce
child 40580 0592d3a39c08
     1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Nov 14 23:55:25 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Nov 15 00:20:36 2010 +0100
     1.3 @@ -19,16 +19,16 @@
     1.4      val ext = "b2i"
     1.5      fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
     1.6      val base_path = add_ext (Path.explode base_name)
     1.7 -    val path_id = Thy_Load.check_file [Thy_Load.master_directory thy] base_path
     1.8 +    val (full_path, _) =
     1.9 +      Thy_Load.check_file [Thy_Load.master_directory thy] base_path
    1.10  
    1.11      val _ = Boogie_VCs.is_closed thy orelse
    1.12        error ("Found the beginning of a new Boogie environment, " ^
    1.13          "but another Boogie environment is still open.")
    1.14    in
    1.15      thy
    1.16 -    |> Thy_Load.require base_path
    1.17 -    |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id)
    1.18 -    |> Thy_Load.provide (base_path, path_id)
    1.19 +    |> Boogie_Loader.load_b2i (not quiet) offsets full_path
    1.20 +    |> Thy_Load.provide_file base_path
    1.21    end
    1.22  
    1.23