# 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));