--- a/src/HOL/Boogie/Tools/boogie_commands.ML Wed Sep 19 13:19:45 2012 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Wed Sep 19 14:47:15 2012 +0200
@@ -16,7 +16,7 @@
fun boogie_open ((quiet, files), offsets) thy =
let
- val ([{src_path = path, text, ...}], thy') = files thy
+ val ([{src_path = path, text, ...}: Token.file], thy') = files thy
val ext = "b2i"
val _ = snd (Path.split_ext path) = ext orelse
--- a/src/HOL/SPARK/Tools/spark_commands.ML Wed Sep 19 13:19:45 2012 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Wed Sep 19 14:47:15 2012 +0200
@@ -15,7 +15,7 @@
fun spark_open header (prfx, files) thy =
let
- val ([{src_path, text = vc_text, pos = vc_pos, ...},
+ val ([{src_path, text = vc_text, pos = vc_pos, ...}: Token.file,
{text = fdl_text, pos = fdl_pos, ...},
{text = rls_text, pos = rls_pos, ...}], thy') = files thy;
val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path));