src/Pure/Isar/outer_syntax.ML

   $$$ "theory" |-- !!! (name -- ($$$ "=" |-- enum1 "+" name) --
     Scan.optional ($$$ "files" |-- !!! (Scan.repeat1 name)) [] --| (Scan.ahead eof || $$$ ":"));
 
 val old_header =
   name -- ($$$ "=" |-- name -- Scan.repeat ($$$ "+" |-- name))
-  >> (fn (A, (B, Bs)) => ((A, B :: Bs), []));
+  >> (fn (A, (B, Bs)) => ((A, B :: Bs), []: string list));
 
 end;
 
 fun deps_thy name ml path =
   let