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