# HG changeset patch
# User wenzelm
# Date 1417438187 -3600
# Node ID 4af6060734d51e6f88318b947fb1c8b8e3a18eb9
# Parent  ec6ce25a630df2e895daca49c295f79fd7d875c4
tuned;

diff -r ec6ce25a630d -r 4af6060734d5 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sun Nov 30 15:11:50 2014 +0100
+++ b/src/Pure/General/scan.ML	Mon Dec 01 13:49:47 2014 +0100
@@ -280,6 +280,7 @@
 datatype lexicon = Lexicon of (bool * lexicon) Symtab.table;
 
 val empty_lexicon = Lexicon Symtab.empty;
+fun is_empty_lexicon (Lexicon tab) = Symtab.is_empty tab;
 
 fun is_literal _ [] = false
   | is_literal (Lexicon tab) (c :: cs) =
@@ -328,7 +329,11 @@
   in append (if tip then rev path' :: content else content) end) tab [];
 
 val dest_lexicon = map implode o dest [];
-fun merge_lexicons (lex1, lex2) = fold extend_lexicon (dest [] lex2) lex1;
+
+fun merge_lexicons (lex1, lex2) =
+  if pointer_eq (lex1, lex2) then lex1
+  else if is_empty_lexicon lex1 then lex2
+  else fold extend_lexicon (dest [] lex2) lex1;
 
 end;