src/Pure/proof_general.ML
changeset 17221 6cd180204582
parent 17217 954c0f265203
child 17314 04e21a27c0ad
     1.1 --- a/src/Pure/proof_general.ML	Thu Sep 01 16:19:02 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Thu Sep 01 18:48:50 2005 +0200
     1.3 @@ -811,11 +811,11 @@
     1.4  
     1.5      fun get_keywords_classification_table () =
     1.6          case (!keywords_classification_table) of
     1.7 -            SOME t => t
     1.8 -          | NONE => (let
     1.9 -                         val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab))
    1.10 -                                         (Symtab.empty,OuterSyntax.dest_parsers())
    1.11 -                     in (keywords_classification_table := SOME tab; tab) end)
    1.12 +          SOME t => t
    1.13 +        | NONE => (let
    1.14 +                     val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k))
    1.15 +                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
    1.16 +                   in (keywords_classification_table := SOME tab; tab) end)
    1.17  
    1.18  
    1.19  
    1.20 @@ -959,7 +959,7 @@
    1.21  
    1.22  fun xmls_of_transition (name,str,toks) =
    1.23     let
    1.24 -       val classification = Symtab.lookup (get_keywords_classification_table(),name)
    1.25 +     val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name
    1.26     in case classification of
    1.27            SOME k => (xmls_of_kind k (name,toks,str))
    1.28          | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)