scan_longid moved to Syntax/lexicon.ML;
authorwenzelm
Fri Oct 10 15:48:43 1997 +0200 (1997-10-10)
changeset 383145e2e7ba31b8
parent 3830 7797327eca1d
child 3832 17a20a2af8f5
scan_longid moved to Syntax/lexicon.ML;
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Fri Oct 10 15:48:10 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Fri Oct 10 15:48:43 1997 +0200
     1.3 @@ -98,8 +98,6 @@
     1.4  
     1.5  (** tokenize **)
     1.6  
     1.7 -val scan_longid = scan_id ^^ (repeat1 ($$ "." ^^ scan_id) >> implode);
     1.8 -
     1.9  fun scan_word lex =
    1.10    max_of
    1.11      (scan_literal lex >> pair Keyword)