# HG changeset patch
# User wenzelm
# Date 1348058835 -7200
# Node ID fad4724230ce141ad8c5eb9da7d4360cc24dc23d
# Parent  75633efcc70da4edac3bd4309b47a97daaf720c0
made SML/NJ happy;

diff -r 75633efcc70d -r fad4724230ce src/HOL/Boogie/Tools/boogie_commands.ML
--- 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
diff -r 75633efcc70d -r fad4724230ce src/HOL/SPARK/Tools/spark_commands.ML
--- 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));