Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SPARK/Tools/spark_commands.ML
changeset 42003 6e45dc518ebb
parent 41948 30732d2390c8
child 42356 e8777e3ea6ef 
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -15,8 +15,7 @@
 
 fun spark_open vc_name thy =
   let
-    val (vc_path, _) = Thy_Load.check_file
-      (Thy_Load.master_directory thy) (Path.explode vc_name);
+    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
         (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
isabelle