tuned;
authorwenzelm
Mon Dec 01 13:49:47 2014 +0100 (2014-12-01)
changeset 590714af6060734d5
parent 59069 ec6ce25a630d
child 59072 27c6936c6484
tuned;
src/Pure/General/scan.ML
     1.1 --- a/src/Pure/General/scan.ML	Sun Nov 30 15:11:50 2014 +0100
     1.2 +++ b/src/Pure/General/scan.ML	Mon Dec 01 13:49:47 2014 +0100
     1.3 @@ -280,6 +280,7 @@
     1.4  datatype lexicon = Lexicon of (bool * lexicon) Symtab.table;
     1.5  
     1.6  val empty_lexicon = Lexicon Symtab.empty;
     1.7 +fun is_empty_lexicon (Lexicon tab) = Symtab.is_empty tab;
     1.8  
     1.9  fun is_literal _ [] = false
    1.10    | is_literal (Lexicon tab) (c :: cs) =
    1.11 @@ -328,7 +329,11 @@
    1.12    in append (if tip then rev path' :: content else content) end) tab [];
    1.13  
    1.14  val dest_lexicon = map implode o dest [];
    1.15 -fun merge_lexicons (lex1, lex2) = fold extend_lexicon (dest [] lex2) lex1;
    1.16 +
    1.17 +fun merge_lexicons (lex1, lex2) =
    1.18 +  if pointer_eq (lex1, lex2) then lex1
    1.19 +  else if is_empty_lexicon lex1 then lex2
    1.20 +  else fold extend_lexicon (dest [] lex2) lex1;
    1.21  
    1.22  end;
    1.23