--- a/src/Pure/Thy/thy_output.ML Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Nov 30 14:02:48 2014 +0100
@@ -671,9 +671,7 @@
verbatim_text ctxt (Input.source_content source)));
fun ml_enclose bg en source =
- ML_Lex.read Position.none bg @
- ML_Lex.read_source false source @
- ML_Lex.read Position.none en;
+ ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
in
@@ -686,7 +684,7 @@
ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *)
(fn source =>
- ML_Lex.read Position.none ("ML_Env.check_functor " ^
+ ML_Lex.read ("ML_Env.check_functor " ^
ML_Syntax.print_string (Input.source_content source))) #>
ml_text @{binding ML_text} (K []));