diff -r c8bac4b0ef07 -r 78df3d65a1cc src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Jan 07 17:32:11 2017 +0100 +++ b/src/Pure/PIDE/command.scala Sat Jan 07 19:36:40 2017 +0100 @@ -351,8 +351,8 @@ // inlined errors case Thy_Header.THEORY => val header = - resources.check_thy_reader("", node_name, - new CharSequenceReader(Token.implode(span.content)), Token.Pos.command) + resources.check_thy_reader( + "", node_name, new CharSequenceReader(Token.implode(span.content))) val errors = for ((imp, pos) <- header.imports if !can_import(imp)) yield { val msg =