# HG changeset patch
# User wenzelm
# Date 1126797425 -7200
# Node ID c56f4809fc6d0fc154045eb34e3ac5fb6ee188b4
# Parent  5093a587da16e839a19d2655b1396f485059ccf5
TableFun/Symtab: curried lookup and update;
nat_option trace_simp_depth_limit;

diff -r 5093a587da16 -r c56f4809fc6d src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Sep 15 17:17:04 2005 +0200
+++ b/src/Pure/proof_general.ML	Thu Sep 15 17:17:05 2005 +0200
@@ -596,6 +596,9 @@
     [("trace-simplifier",
       ("Trace simplification rules.",
        bool_option trace_simp)),
+     ("trace-simplifier-depth",
+      ("Trace simplifier depth limit.",
+       nat_option trace_simp_depth_limit)),
      ("trace-rules",
       ("Trace application of the standard rules",
        bool_option trace_rules)),
@@ -813,7 +816,7 @@
         case (!keywords_classification_table) of
           SOME t => t
         | NONE => (let
-                     val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k))
+                     val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
                                     (OuterSyntax.dest_parsers ()) Symtab.empty;
                    in (keywords_classification_table := SOME tab; tab) end)
 
@@ -959,7 +962,7 @@
 
 fun xmls_of_transition (name,str,toks) =
    let
-     val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name
+     val classification = Symtab.lookup (get_keywords_classification_table ()) name
    in case classification of
           SOME k => (xmls_of_kind k (name,toks,str))
         | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)