src/Pure/Thy/thy_output.ML

   (fn {context = ctxt, ...} => fn source =>
    (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
     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
 
 val _ = Theory.setup
  (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>

   ml_text @{binding ML_structure}
     (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
 
   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 []));
 
 end;