# HG changeset patch
# User wenzelm
# Date 1551037457 -3600
# Node ID b3c9291b5fc7858aa837391272d2176a8c4b6b78
# Parent  a35033167f0176ea78485b7afc86aefb98bda74d
clarified signature, notably for hol4isabelle (by Fabian Immler);

diff -r a35033167f01 -r b3c9291b5fc7 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Feb 24 13:00:43 2019 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Feb 24 20:44:17 2019 +0100
@@ -34,6 +34,7 @@
     token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
   val read_source: Input.source -> token Antiquote.antiquote list
   val read_source_sml: Input.source -> token Antiquote.antiquote list
+  val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
@@ -383,6 +384,8 @@
   read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
     scan_sml_antiq;
 
+val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
+
 end;
 
 end;