clarified signature, notably for hol4isabelle (by Fabian Immler);
authorwenzelm
Sun Feb 24 20:44:17 2019 +0100 (4 months ago ago)
changeset 70022b3c9291b5fc7
parent 70021 a35033167f01
child 70023 9a7f94ab4df9
clarified signature, notably for hol4isabelle (by Fabian Immler);
src/Pure/ML/ml_lex.ML
     1.1 --- a/src/Pure/ML/ml_lex.ML	Sun Feb 24 13:00:43 2019 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Feb 24 20:44:17 2019 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4      token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
     1.5    val read_source: Input.source -> token Antiquote.antiquote list
     1.6    val read_source_sml: Input.source -> token Antiquote.antiquote list
     1.7 +  val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
     1.8  end;
     1.9  
    1.10  structure ML_Lex: ML_LEX =
    1.11 @@ -383,6 +384,8 @@
    1.12    read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
    1.13      scan_sml_antiq;
    1.14  
    1.15 +val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
    1.16 +
    1.17  end;
    1.18  
    1.19  end;