diff -r ac7097bd8611 -r 6e45dc518ebb src/HOL/SPARK/Tools/spark_commands.ML
--- 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 ())