# HG changeset patch
# User wenzelm
# Date 932156707 -7200
# Node ID afbd8241797b6515baf643e931245c6c4c5ead39
# Parent  44bd3c094fd6e98be604e5b6cbeb62ec3d640d5f
tuned dest_lexicon;

diff -r 44bd3c094fd6 -r afbd8241797b src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Fri Jul 16 22:24:42 1999 +0200
+++ b/src/Pure/General/scan.ML	Fri Jul 16 22:25:07 1999 +0200
@@ -60,7 +60,7 @@
   val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   type lexicon
-  val dest_lexicon: lexicon -> string list list
+  val dest_lexicon: lexicon -> string list
   val make_lexicon: string list list -> lexicon
   val empty_lexicon: lexicon
   val extend_lexicon: lexicon -> string list list -> lexicon
@@ -240,11 +240,13 @@
 
 (* dest_lexicon *)
 
-fun dest_lexicon Empty = []
-  | dest_lexicon (Branch (_, [], lt, eq, gt)) =
-      dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
-  | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
-      dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
+fun dest_lex Empty = []
+  | dest_lex (Branch (_, [], lt, eq, gt)) =
+      dest_lex lt @ dest_lex eq @ dest_lex gt
+  | dest_lex (Branch (_, cs, lt, eq, gt)) =
+      dest_lex lt @ [cs] @ dest_lex eq @ dest_lex gt;
+
+val dest_lexicon = map implode o dest_lex;
 
 
 (* empty, extend, make, merge lexicons *)
@@ -265,14 +267,14 @@
 	      Branch (c, no_literal, Empty, add Empty cs, Empty)
 	  | add lex [] = lex;
       in add lex chrs end;
-  in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
+  in foldl ext (lexicon, chrss \\ dest_lex lexicon) end;
 
 val make_lexicon = extend_lexicon empty_lexicon;
 
 fun merge_lexicons lex1 lex2 =
   let
-    val chss1 = dest_lexicon lex1;
-    val chss2 = dest_lexicon lex2;
+    val chss1 = dest_lex lex1;
+    val chss2 = dest_lex lex2;
   in
     if chss2 subset chss1 then lex1
     else if chss1 subset chss2 then lex2
diff -r 44bd3c094fd6 -r afbd8241797b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jul 16 22:24:42 1999 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jul 16 22:25:07 1999 +0200
@@ -281,7 +281,7 @@
     val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
     val prmodes' = sort_strings (filter_out (equal "") prmodes);
   in
-    Pretty.writeln (pretty_strs_qs "lexicon:" (map implode (Scan.dest_lexicon lexicon)));
+    Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon));
     Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
     Pretty.writeln (pretty_strs_qs "print modes:" prmodes')