# HG changeset patch
# User wenzelm
# Date 876491323 -7200
# Node ID 45e2e7ba31b83f09613bc7f574b9b595ee92cf2a
# Parent  7797327eca1d3cd33b27b784a39c51e84d5faceb
scan_longid moved to Syntax/lexicon.ML;

diff -r 7797327eca1d -r 45e2e7ba31b8 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Fri Oct 10 15:48:10 1997 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Fri Oct 10 15:48:43 1997 +0200
@@ -98,8 +98,6 @@
 
 (** tokenize **)
 
-val scan_longid = scan_id ^^ (repeat1 ($$ "." ^^ scan_id) >> implode);
-
 fun scan_word lex =
   max_of
     (scan_literal lex >> pair Keyword)