# HG changeset patch
# User wenzelm
# Date 1299174132 -3600
# Node ID ececcbd08d352a8a411367dbaa8935debbb74596
# Parent  aa8dce9ab8a9b6ae5ac30b038551a81c5eb11c41
simplified Thy_Info.check_file -- discontinued load path;

diff -r aa8dce9ab8a9 -r ececcbd08d35 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Mar 03 18:10:28 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Mar 03 18:42:12 2011 +0100
@@ -23,7 +23,7 @@
 
     val base_path = Path.explode base_name |> tap check_ext
     val (full_path, _) =
-      Thy_Load.check_file [Thy_Load.master_directory thy] base_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, " ^
diff -r aa8dce9ab8a9 -r ececcbd08d35 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Thu Mar 03 18:10:28 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Thu Mar 03 18:42:12 2011 +0100
@@ -18,8 +18,9 @@
 fun spark_open vc_name thy =
   let
     val (vc_path, _) = Thy_Load.check_file
-      [Thy_Load.master_directory thy] (Path.explode vc_name);
-    val (base, header) = (case Path.split_ext vc_path of
+      (Thy_Load.master_directory thy) (Path.explode vc_name);
+    val (base, header) =
+      (case Path.split_ext vc_path of
         (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
       | (base, "siv") => (base, Fdl_Lexer.siv_header >> K ())
       | _ => error "File name must end with .vcg or .siv");