curried_lookup/update;
authorwenzelm
Thu Sep 01 18:48:50 2005 +0200 (2005-09-01)
changeset 172216cd180204582
parent 17220 b41d8e290bf8
child 17222 819bc7f22423
curried_lookup/update;
src/Pure/General/graph.ML
src/Pure/General/name_space.ML
src/Pure/General/output.ML
src/Pure/General/symbol.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/term_style.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_parse.ML
src/Pure/axclass.ML
src/Pure/compress.ML
src/Pure/context.ML
src/Pure/fact_index.ML
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/proof_general.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/graph.ML	Thu Sep 01 16:19:02 2005 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Thu Sep 01 18:48:50 2005 +0200
     1.3 @@ -86,11 +86,11 @@
     1.4  fun maximals (Graph tab) = Table.fold (fn (m, (_, (_, []))) => cons m | _ => I) tab [];
     1.5  
     1.6  fun get_entry (Graph tab) x =
     1.7 -  (case Table.lookup (tab, x) of
     1.8 +  (case Table.curried_lookup tab x of
     1.9      SOME entry => entry
    1.10    | NONE => raise UNDEF x);
    1.11  
    1.12 -fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab));
    1.13 +fun map_entry x f (G as Graph tab) = Graph (Table.curried_update (x, f (get_entry G x)) tab);
    1.14  
    1.15  
    1.16  (* nodes *)
    1.17 @@ -142,7 +142,7 @@
    1.18  (* nodes *)
    1.19  
    1.20  fun new_node (x, info) (Graph tab) =
    1.21 -  Graph (Table.update_new ((x, (info, ([], []))), tab));
    1.22 +  Graph (Table.curried_update_new (x, (info, ([], []))) tab);
    1.23  
    1.24  fun default_node (x, info) (Graph tab) =
    1.25    Graph (Table.default (x, (info, ([], []))) tab);
     2.1 --- a/src/Pure/General/name_space.ML	Thu Sep 01 16:19:02 2005 +0200
     2.2 +++ b/src/Pure/General/name_space.ML	Thu Sep 01 18:48:50 2005 +0200
     2.3 @@ -113,7 +113,7 @@
     2.4  val empty = NameSpace Symtab.empty;
     2.5  
     2.6  fun lookup (NameSpace tab) xname =
     2.7 -  (case Symtab.lookup (tab, xname) of
     2.8 +  (case Symtab.curried_lookup tab xname of
     2.9      NONE => (xname, true)
    2.10    | SOME ([], []) => (xname, true)
    2.11    | SOME ([name], _) => (name, true)
    2.12 @@ -150,7 +150,7 @@
    2.13  (* basic operations *)
    2.14  
    2.15  fun map_space f xname (NameSpace tab) =
    2.16 -  NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
    2.17 +  NameSpace (Symtab.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab);
    2.18  
    2.19  fun del (name: string) = remove (op =) name;
    2.20  fun add name names = name :: del name names;
     3.1 --- a/src/Pure/General/output.ML	Thu Sep 01 16:19:02 2005 +0200
     3.2 +++ b/src/Pure/General/output.ML	Thu Sep 01 18:48:50 2005 +0200
     3.3 @@ -84,7 +84,7 @@
     3.4  
     3.5  exception MISSING_DEFAULT_OUTPUT;
     3.6  
     3.7 -fun lookup_mode name = Symtab.lookup (! modes, name);
     3.8 +fun lookup_mode name = Symtab.curried_lookup (! modes) name;
     3.9  
    3.10  fun get_mode () =
    3.11    (case Library.get_first lookup_mode (! print_mode) of SOME p => p
    3.12 @@ -141,7 +141,7 @@
    3.13  fun add_mode name (f, g, h) =
    3.14   (if is_none (lookup_mode name) then ()
    3.15    else warning ("Redeclaration of symbol print mode: " ^ quote name);
    3.16 -  modes := Symtab.update ((name, {output_width = f, indent = g, raw = h}), ! modes));
    3.17 +  modes := Symtab.curried_update (name, {output_width = f, indent = g, raw = h}) (! modes));
    3.18  
    3.19  
    3.20  (* produce errors *)
     4.1 --- a/src/Pure/General/symbol.ML	Thu Sep 01 16:19:02 2005 +0200
     4.2 +++ b/src/Pure/General/symbol.ML	Thu Sep 01 18:48:50 2005 +0200
     4.3 @@ -350,7 +350,7 @@
     4.4      else if is_ascii_quasi s then Quasi
     4.5      else if is_ascii_blank s then Blank
     4.6      else if is_char s then Other
     4.7 -    else if_none (Symtab.lookup (symbol_kinds, s)) Other;
     4.8 +    else if_none (Symtab.curried_lookup symbol_kinds s) Other;
     4.9  end;
    4.10  
    4.11  fun is_letter s = kind s = Letter;
     5.1 --- a/src/Pure/Isar/attrib.ML	Thu Sep 01 16:19:02 2005 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Thu Sep 01 18:48:50 2005 +0200
     5.3 @@ -104,7 +104,7 @@
     5.4      val attrs = #2 (AttributesData.get thy);
     5.5      fun attr src =
     5.6        let val ((name, _), pos) = Args.dest_src src in
     5.7 -        (case Symtab.lookup (attrs, name) of
     5.8 +        (case Symtab.curried_lookup attrs name of
     5.9            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    5.10          | SOME ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src))
    5.11        end;
     6.1 --- a/src/Pure/Isar/isar_output.ML	Thu Sep 01 16:19:02 2005 +0200
     6.2 +++ b/src/Pure/Isar/isar_output.ML	Thu Sep 01 18:48:50 2005 +0200
     6.3 @@ -59,7 +59,7 @@
     6.4  fun add_item kind (name, x) tab =
     6.5   (if not (Symtab.defined tab name) then ()
     6.6    else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name);
     6.7 -  Symtab.update ((name, x), tab));
     6.8 +  Symtab.curried_update (name, x) tab);
     6.9  
    6.10  in
    6.11  
    6.12 @@ -68,13 +68,13 @@
    6.13  
    6.14  fun command src =
    6.15    let val ((name, _), pos) = Args.dest_src src in
    6.16 -    (case Symtab.lookup (! global_commands, name) of
    6.17 +    (case Symtab.curried_lookup (! global_commands) name of
    6.18        NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
    6.19      | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
    6.20    end;
    6.21  
    6.22  fun option (name, s) f () =
    6.23 -  (case Symtab.lookup (! global_options, name) of
    6.24 +  (case Symtab.curried_lookup (! global_options) name of
    6.25      NONE => error ("Unknown antiquotation option: " ^ quote name)
    6.26    | SOME opt => opt s f ());
    6.27  
     7.1 --- a/src/Pure/Isar/locale.ML	Thu Sep 01 16:19:02 2005 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Thu Sep 01 18:48:50 2005 +0200
     7.3 @@ -168,7 +168,7 @@
     7.4  fun tinst_tab_type tinst T = if Symtab.is_empty tinst
     7.5        then T
     7.6        else Term.map_type_tfree
     7.7 -        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
     7.8 +        (fn (v as (x, _)) => getOpt (Symtab.curried_lookup tinst x, (TFree v))) T;
     7.9  
    7.10  fun tinst_tab_term tinst t = if Symtab.is_empty tinst
    7.11        then t
    7.12 @@ -201,7 +201,7 @@
    7.13        else (* instantiate terms and types simultaneously *)
    7.14          let
    7.15            fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
    7.16 -            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
    7.17 +            | instf (Free (x, T)) = (case Symtab.curried_lookup inst x of
    7.18                   NONE => Free (x, tinst_tab_type tinst T)
    7.19                 | SOME t => t)
    7.20              | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
    7.21 @@ -322,7 +322,7 @@
    7.22                  val sups =
    7.23                    List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
    7.24                  val sups' = map (apfst untermify) sups
    7.25 -              in (Termtab.update ((t, (attn, [])), regs), sups') end
    7.26 +              in (Termtab.curried_update (t, (attn, [])) regs, sups') end
    7.27        | _ => (regs, []))
    7.28      end;
    7.29  
    7.30 @@ -331,9 +331,9 @@
    7.31    fun add_witness ts thm regs =
    7.32      let
    7.33        val t = termify ts;
    7.34 -      val (x, thms) = valOf (Termtab.lookup (regs, t));
    7.35 +      val (x, thms) = valOf (Termtab.curried_lookup regs t);
    7.36      in
    7.37 -      Termtab.update ((t, (x, thm::thms)), regs)
    7.38 +      Termtab.curried_update (t, (x, thm::thms)) regs
    7.39      end;
    7.40  end;
    7.41  
    7.42 @@ -398,9 +398,9 @@
    7.43  
    7.44  fun put_locale name loc =
    7.45    GlobalLocalesData.map (fn (space, locs, regs) =>
    7.46 -    (space, Symtab.update ((name, loc), locs), regs));
    7.47 +    (space, Symtab.curried_update (name, loc) locs, regs));
    7.48  
    7.49 -fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name);
    7.50 +fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name;
    7.51  
    7.52  fun the_locale thy name =
    7.53    (case get_locale thy name of
    7.54 @@ -417,7 +417,7 @@
    7.55  (* retrieve registration from theory or context *)
    7.56  
    7.57  fun gen_get_registrations get thy_ctxt name =
    7.58 -  case Symtab.lookup (get thy_ctxt, name) of
    7.59 +  case Symtab.curried_lookup (get thy_ctxt) name of
    7.60        NONE => []
    7.61      | SOME reg => Registrations.dest reg;
    7.62  
    7.63 @@ -427,7 +427,7 @@
    7.64       gen_get_registrations LocalLocalesData.get;
    7.65  
    7.66  fun gen_get_registration get thy_of thy_ctxt (name, ps) =
    7.67 -  case Symtab.lookup (get thy_ctxt, name) of
    7.68 +  case Symtab.curried_lookup (get thy_ctxt) name of
    7.69        NONE => NONE
    7.70      | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
    7.71  
    7.72 @@ -452,7 +452,7 @@
    7.73    map_data (fn regs =>
    7.74      let
    7.75        val thy = thy_of thy_ctxt;
    7.76 -      val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
    7.77 +      val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty);
    7.78        val (reg', sups) = Registrations.insert thy (ps, attn) reg;
    7.79        val _ = if not (null sups) then warning
    7.80                  ("Subsumed interpretation(s) of locale " ^
    7.81 @@ -460,7 +460,7 @@
    7.82                   "\nby interpretation(s) with the following prefix(es):\n" ^
    7.83                    commas_quote (map (fn (_, ((s, _), _)) => s) sups))
    7.84                else ();
    7.85 -    in Symtab.update ((name, reg'), regs) end) thy_ctxt;
    7.86 +    in Symtab.curried_update (name, reg') regs end) thy_ctxt;
    7.87  
    7.88  val put_global_registration =
    7.89       gen_put_registration (fn f =>
    7.90 @@ -480,13 +480,8 @@
    7.91  (* add witness theorem to registration in theory or context,
    7.92     ignored if registration not present *)
    7.93  
    7.94 -fun gen_add_witness map (name, ps) thm =
    7.95 -  map (fn regs =>
    7.96 -      let
    7.97 -        val reg = valOf (Symtab.lookup (regs, name));
    7.98 -      in
    7.99 -        Symtab.update ((name, Registrations.add_witness ps thm reg), regs)
   7.100 -      end handle Option => regs);
   7.101 +fun gen_add_witness map_regs (name, ps) thm =
   7.102 +  map_regs (Symtab.map_entry name (Registrations.add_witness ps thm));
   7.103  
   7.104  val add_global_witness =
   7.105       gen_add_witness (fn f =>
   7.106 @@ -550,7 +545,7 @@
   7.107  
   7.108      val loc_int = intern thy loc;
   7.109      val regs = get_regs thy_ctxt;
   7.110 -    val loc_regs = Symtab.lookup (regs, loc_int);
   7.111 +    val loc_regs = Symtab.curried_lookup regs loc_int;
   7.112    in
   7.113      (case loc_regs of
   7.114          NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
   7.115 @@ -762,7 +757,7 @@
   7.116  fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
   7.117  fun params_syn_of syn elemss =
   7.118    gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
   7.119 -    map (apfst (fn x => (x, valOf (Symtab.lookup (syn, x)))));
   7.120 +    map (apfst (fn x => (x, valOf (Symtab.curried_lookup syn x))));
   7.121  
   7.122  
   7.123  (* CB: param_types has the following type:
   7.124 @@ -1008,7 +1003,7 @@
   7.125          val {params = (ps, qs), elems, ...} = the_locale thy name;
   7.126          val ps' = map (apsnd SOME o #1) ps;
   7.127          val ren = map #1 ps' ~~
   7.128 -              map (fn x => (x, valOf (Symtab.lookup (syn, x)))) xs;
   7.129 +              map (fn x => (x, valOf (Symtab.curried_lookup syn x))) xs;
   7.130          val (params', elems') =
   7.131            if null ren then ((ps', qs), map #1 elems)
   7.132            else ((map (apfst (rename ren)) ps', map (rename ren) qs),
   7.133 @@ -1740,7 +1735,7 @@
   7.134          |> Symtab.make;            
   7.135      (* replace parameter names in ids by instantiations *)
   7.136      val vinst = Symtab.make (parms ~~ vts);
   7.137 -    fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
   7.138 +    fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps;
   7.139      val inst = Symtab.make (parms ~~ ts);
   7.140      val ids' = map (apsnd vinst_names) ids;
   7.141      val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
   7.142 @@ -2008,7 +2003,7 @@
   7.143      |> put_locale name {predicate = predicate, import = import,
   7.144          elems = map (fn e => (e, stamp ())) elems',
   7.145          params = (params_of elemss' |>
   7.146 -          map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)),
   7.147 +          map (fn (x, SOME T) => ((x, T), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)),
   7.148          regs = []}
   7.149      |> pair (elems', body_ctxt)
   7.150    end;
   7.151 @@ -2177,7 +2172,7 @@
   7.152                 NONE => error ("Instance missing for parameter " ^ quote p)
   7.153               | SOME (Free (_, T), t) => (t, T);
   7.154          val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
   7.155 -      in (Symtab.update_new ((p, d), inst), tinst) end;
   7.156 +      in (Symtab.curried_update_new (p, d) inst, tinst) end;
   7.157      val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
   7.158      (* Note: inst and tinst contain no vars. *)
   7.159  
     8.1 --- a/src/Pure/Isar/method.ML	Thu Sep 01 16:19:02 2005 +0200
     8.2 +++ b/src/Pure/Isar/method.ML	Thu Sep 01 18:48:50 2005 +0200
     8.3 @@ -560,7 +560,7 @@
     8.4          val ((raw_name, _), pos) = Args.dest_src src;
     8.5          val name = NameSpace.intern space raw_name;
     8.6        in
     8.7 -        (case Symtab.lookup (meths, name) of
     8.8 +        (case Symtab.curried_lookup meths name of
     8.9            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    8.10          | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
    8.11        end;
     9.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Sep 01 16:19:02 2005 +0200
     9.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Sep 01 18:48:50 2005 +0200
     9.3 @@ -125,10 +125,10 @@
     9.4  
     9.5  fun get_lexicons () = ! global_lexicons;
     9.6  fun get_parsers () = ! global_parsers;
     9.7 -fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (get_parsers ());
     9.8 +fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ());
     9.9  
    9.10  fun command_tags name =
    9.11 -  (case Symtab.lookup (get_parsers (), name) of
    9.12 +  (case Symtab.curried_lookup (get_parsers ()) name of
    9.13      SOME (((_, k), _), _) => OuterKeyword.tags_of k
    9.14    | NONE => []);
    9.15  
    9.16 @@ -143,7 +143,7 @@
    9.17  fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
    9.18   (if not (Symtab.defined tab name) then ()
    9.19    else warning ("Redefined outer syntax command " ^ quote name);
    9.20 -  Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
    9.21 +  Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab);
    9.22  
    9.23  fun add_parsers parsers =
    9.24    (change_parsers (fold add_parser parsers);
    10.1 --- a/src/Pure/Isar/proof_context.ML	Thu Sep 01 16:19:02 2005 +0200
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Sep 01 18:48:50 2005 +0200
    10.3 @@ -364,18 +364,18 @@
    10.4  
    10.5  (** default sorts and types **)
    10.6  
    10.7 -fun def_sort ctxt xi = Vartab.lookup (#2 (defaults_of ctxt), xi);
    10.8 +val def_sort = Vartab.curried_lookup o #2 o defaults_of;
    10.9  
   10.10  fun def_type ctxt pattern xi =
   10.11    let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in
   10.12 -    (case Vartab.lookup (types, xi) of
   10.13 +    (case Vartab.curried_lookup types xi of
   10.14        NONE =>
   10.15          if pattern then NONE
   10.16 -        else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2)
   10.17 +        else Vartab.curried_lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2)
   10.18      | some => some)
   10.19    end;
   10.20  
   10.21 -fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt), (x, ~1));
   10.22 +fun default_type ctxt x = Vartab.curried_lookup (#1 (defaults_of ctxt)) (x, ~1);
   10.23  val used_types = #3 o defaults_of;
   10.24  
   10.25  
   10.26 @@ -492,7 +492,7 @@
   10.27  
   10.28      val binds = binds_of ctxt;
   10.29      fun norm (t as Var (xi, T)) =
   10.30 -          (case Vartab.lookup (binds, xi) of
   10.31 +          (case Vartab.curried_lookup binds xi of
   10.32              SOME (u, U) =>
   10.33                let
   10.34                  val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
   10.35 @@ -596,24 +596,24 @@
   10.36  local
   10.37  
   10.38  val ins_types = fold_aterms
   10.39 -  (fn Free (x, T) => curry Vartab.update ((x, ~1), T)
   10.40 -    | Var v => curry Vartab.update v
   10.41 +  (fn Free (x, T) => Vartab.curried_update ((x, ~1), T)
   10.42 +    | Var v => Vartab.curried_update v
   10.43      | _ => I);
   10.44  
   10.45  val ins_sorts = fold_types (fold_atyps
   10.46 -  (fn TFree (x, S) => curry Vartab.update ((x, ~1), S)
   10.47 -    | TVar v => curry Vartab.update v
   10.48 +  (fn TFree (x, S) => Vartab.curried_update ((x, ~1), S)
   10.49 +    | TVar v => Vartab.curried_update v
   10.50      | _ => I));
   10.51  
   10.52  val ins_used = fold_term_types (fn t =>
   10.53    fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I));
   10.54  
   10.55  val ins_occs = fold_term_types (fn t =>
   10.56 -  fold_atyps (fn TFree (x, _) => curry Symtab.update_multi (x, t) | _ => I));
   10.57 +  fold_atyps (fn TFree (x, _) => Symtab.curried_update_multi (x, t) | _ => I));
   10.58  
   10.59  fun ins_skolem def_ty = fold_rev (fn (x, x') =>
   10.60    (case def_ty x' of
   10.61 -    SOME T => curry Vartab.update ((x, ~1), T)
   10.62 +    SOME T => Vartab.curried_update ((x, ~1), T)
   10.63    | NONE => I));
   10.64  
   10.65  fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   10.66 @@ -632,7 +632,7 @@
   10.67    |> declare_term_syntax t
   10.68    |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
   10.69    |> map_defaults (fn (types, sorts, used, occ) =>
   10.70 -      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes_of ctxt) types,
   10.71 +      (ins_skolem (fn x => Vartab.curried_lookup types (x, ~1)) (fixes_of ctxt) types,
   10.72          sorts, used, occ));
   10.73  
   10.74  end;
   10.75 @@ -690,7 +690,7 @@
   10.76      val occs_outer = type_occs_of outer;
   10.77      fun add a gen =
   10.78        if Symtab.defined occs_outer a orelse
   10.79 -        exists still_fixed (Symtab.lookup_multi (occs_inner, a))
   10.80 +        exists still_fixed (Symtab.curried_lookup_multi occs_inner a)
   10.81        then gen else a :: gen;
   10.82    in fn tfrees => fold add tfrees [] end;
   10.83  
   10.84 @@ -777,7 +777,7 @@
   10.85        else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   10.86    in
   10.87      map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   10.88 -      (syntax, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs))
   10.89 +      (syntax, asms, Vartab.curried_update ((x, i), (t', T)) binds, thms, cases, defs))
   10.90      o declare_term t'
   10.91    end;
   10.92  
   10.93 @@ -935,7 +935,7 @@
   10.94          val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
   10.95          val name = PureThy.name_of_thmref thmref;
   10.96        in
   10.97 -        (case Symtab.lookup (tab, name) of
   10.98 +        (case Symtab.curried_lookup tab name of
   10.99            SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
  10.100          | NONE => from_thy thy xthmref) |> pick name
  10.101        end
  10.102 @@ -990,7 +990,7 @@
  10.103          let
  10.104            val name = NameSpace.full naming bname;
  10.105            val space' = NameSpace.declare naming name space;
  10.106 -          val tab' = Symtab.update ((name, ths), tab);
  10.107 +          val tab' = Symtab.curried_update (name, ths) tab;
  10.108            val index' = FactIndex.add (is_known ctxt) (name, ths) index;
  10.109          in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
  10.110  
    11.1 --- a/src/Pure/Isar/term_style.ML	Thu Sep 01 16:19:02 2005 +0200
    11.2 +++ b/src/Pure/Isar/term_style.ML	Thu Sep 01 18:48:50 2005 +0200
    11.3 @@ -2,7 +2,8 @@
    11.4      ID:         $Id$
    11.5      Author:     Florian Haftmann, TU Muenchen
    11.6  
    11.7 -Styles for terms, to use with the "term_style" and "thm_style" antiquotations.
    11.8 +Styles for terms, to use with the "term_style" and "thm_style"
    11.9 +antiquotations.
   11.10  *)
   11.11  
   11.12  signature TERM_STYLE =
   11.13 @@ -39,12 +40,12 @@
   11.14  (* accessors *)
   11.15  
   11.16  fun the_style thy name =
   11.17 -  (case Symtab.lookup (StyleData.get thy, name) of
   11.18 +  (case Symtab.curried_lookup (StyleData.get thy) name of
   11.19      NONE => error ("Unknown antiquote style: " ^ quote name)
   11.20    | SOME (style, _) => style);
   11.21  
   11.22  fun add_style name style thy =
   11.23 -  StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
   11.24 +  StyleData.map (Symtab.curried_update_new (name, (style, stamp ()))) thy
   11.25      handle Symtab.DUP _ => err_dup_styles [name];
   11.26  
   11.27  
    12.1 --- a/src/Pure/Syntax/ast.ML	Thu Sep 01 16:19:02 2005 +0200
    12.2 +++ b/src/Pure/Syntax/ast.ML	Thu Sep 01 18:48:50 2005 +0200
    12.3 @@ -157,7 +157,7 @@
    12.4            if a = b then env else raise NO_MATCH
    12.5        | mtch (Variable a) (Constant b) env =
    12.6            if a = b then env else raise NO_MATCH
    12.7 -      | mtch ast (Variable x) env = Symtab.update ((x, ast), env)
    12.8 +      | mtch ast (Variable x) env = Symtab.curried_update (x, ast) env
    12.9        | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
   12.10        | mtch _ _ _ = raise NO_MATCH
   12.11      and mtch_lst (ast :: asts) (pat :: pats) env =
   12.12 @@ -189,7 +189,7 @@
   12.13      val changes = ref 0;
   12.14  
   12.15      fun subst _ (ast as Constant _) = ast
   12.16 -      | subst env (Variable x) = the (Symtab.lookup (env, x))
   12.17 +      | subst env (Variable x) = the (Symtab.curried_lookup env x)
   12.18        | subst env (Appl asts) = Appl (map (subst env) asts);
   12.19  
   12.20      fun try_rules ((lhs, rhs) :: pats) ast =
    13.1 --- a/src/Pure/Syntax/parser.ML	Thu Sep 01 16:19:02 2005 +0200
    13.2 +++ b/src/Pure/Syntax/parser.ML	Thu Sep 01 18:48:50 2005 +0200
    13.3 @@ -446,9 +446,9 @@
    13.4    let
    13.5      (*Get tag for existing nonterminal or create a new one*)
    13.6      fun get_tag nt_count tags nt =
    13.7 -      case Symtab.lookup (tags, nt) of
    13.8 +      case Symtab.curried_lookup tags nt of
    13.9          SOME tag => (nt_count, tags, tag)
   13.10 -      | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
   13.11 +      | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
   13.12                   nt_count);
   13.13  
   13.14      (*Convert symbols to the form used by the parser;
   13.15 @@ -523,9 +523,9 @@
   13.16  
   13.17      (*get existing tag from grammar1 or create a new one*)
   13.18      fun get_tag nt_count tags nt =
   13.19 -      case Symtab.lookup (tags, nt) of
   13.20 +      case Symtab.curried_lookup tags nt of
   13.21          SOME tag => (nt_count, tags, tag)
   13.22 -      | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
   13.23 +      | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
   13.24                  nt_count)
   13.25  
   13.26      val ((nt_count1', tags1'), tag_table) =
   13.27 @@ -868,7 +868,7 @@
   13.28  
   13.29  fun earley prods tags chains startsymbol indata =
   13.30    let
   13.31 -    val start_tag = case Symtab.lookup (tags, startsymbol) of
   13.32 +    val start_tag = case Symtab.curried_lookup tags startsymbol of
   13.33                         SOME tag => tag
   13.34                       | NONE   => error ("parse: Unknown startsymbol " ^
   13.35                                          quote startsymbol);
    14.1 --- a/src/Pure/Syntax/printer.ML	Thu Sep 01 16:19:02 2005 +0200
    14.2 +++ b/src/Pure/Syntax/printer.ML	Thu Sep 01 18:48:50 2005 +0200
    14.3 @@ -248,7 +248,7 @@
    14.4      val tab = fold f fmts (mode_tab prtabs mode);
    14.5    in AList.update (op =) (mode, tab) prtabs end;
    14.6  
    14.7 -fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m;
    14.8 +fun extend_prtabs m = change_prtabs Symtab.curried_update_multi m;
    14.9  fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
   14.10  
   14.11  fun merge_prtabs prtabs1 prtabs2 =
   14.12 @@ -330,7 +330,7 @@
   14.13  
   14.14          (*find matching table entry, or print as prefix / postfix*)
   14.15          fun prnt ([], []) = prefixT tup
   14.16 -          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi (tb, a), tbs)
   14.17 +          | prnt ([], tb :: tbs) = prnt (Symtab.curried_lookup_multi tb a, tbs)
   14.18            | prnt ((pr, n, p') :: prnps, tbs) =
   14.19                if nargs = n then parT (pr, args, p, p')
   14.20                else if nargs > n andalso not type_mode then
    15.1 --- a/src/Pure/Syntax/syntax.ML	Thu Sep 01 16:19:02 2005 +0200
    15.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Sep 01 18:48:50 2005 +0200
    15.3 @@ -82,7 +82,7 @@
    15.4  
    15.5  (* parse (ast) translations *)
    15.6  
    15.7 -fun lookup_tr tab c = Option.map fst (Symtab.lookup (tab, c));
    15.8 +fun lookup_tr tab c = Option.map fst (Symtab.curried_lookup tab c);
    15.9  
   15.10  fun err_dup_trfuns name cs =
   15.11    error ("More than one " ^ name ^ " for " ^ commas_quote cs);
   15.12 @@ -98,8 +98,8 @@
   15.13  
   15.14  (* print (ast) translations *)
   15.15  
   15.16 -fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
   15.17 -fun extend_tr'tab trfuns = fold_rev (curry Symtab.update_multi) trfuns;
   15.18 +fun lookup_tr' tab c = map fst (Symtab.curried_lookup_multi tab c);
   15.19 +fun extend_tr'tab trfuns = fold_rev Symtab.curried_update_multi trfuns;
   15.20  fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
   15.21  fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
   15.22  
   15.23 @@ -147,16 +147,12 @@
   15.24  type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
   15.25  
   15.26  fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab));
   15.27 -fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a);
   15.28  
   15.29  
   15.30  (* empty, extend, merge ruletabs *)
   15.31  
   15.32 -val extend_ruletab =
   15.33 -  fold_rev (fn r => fn tab => Symtab.update_multi ((Ast.head_of_rule r, r), tab));
   15.34 -
   15.35 +val extend_ruletab = fold_rev (fn r => Symtab.curried_update_multi (Ast.head_of_rule r, r));
   15.36  val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
   15.37 -
   15.38  fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
   15.39  
   15.40  
   15.41 @@ -389,7 +385,7 @@
   15.42      val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   15.43    in
   15.44      SynTrans.asts_to_terms thy (lookup_tr parse_trtab)
   15.45 -      (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
   15.46 +      (map (Ast.normalize_ast (Symtab.curried_lookup_multi parse_ruletab)) asts)
   15.47    end;
   15.48  
   15.49  
   15.50 @@ -473,7 +469,7 @@
   15.51    in
   15.52      prt_t thy curried prtabs (lookup_tr' print_ast_trtab)
   15.53        (lookup_tokentr tokentrtab (! print_mode))
   15.54 -      (Ast.normalize_ast (lookup_ruletab print_ruletab) ast)
   15.55 +      (Ast.normalize_ast (Symtab.curried_lookup_multi print_ruletab) ast)
   15.56    end;
   15.57  
   15.58  val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
    16.1 --- a/src/Pure/Thy/html.ML	Thu Sep 01 16:19:02 2005 +0200
    16.2 +++ b/src/Pure/Thy/html.ML	Thu Sep 01 18:48:50 2005 +0200
    16.3 @@ -205,7 +205,7 @@
    16.4    fun output_sym s =
    16.5      if Symbol.is_raw s then (1.0, Symbol.decode_raw s)
    16.6      else
    16.7 -      (case Symtab.lookup (html_syms, s) of SOME x => x
    16.8 +      (case Symtab.curried_lookup html_syms s of SOME x => x
    16.9        | NONE => (real (size s), translate_string escape s));
   16.10  
   16.11    fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
    17.1 --- a/src/Pure/Thy/present.ML	Thu Sep 01 16:19:02 2005 +0200
    17.2 +++ b/src/Pure/Thy/present.ML	Thu Sep 01 18:48:50 2005 +0200
    17.3 @@ -172,13 +172,13 @@
    17.4  
    17.5  fun init_theory_info name info =
    17.6    change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    17.7 -    (Symtab.update ((name, info), theories), files, tex_index, html_index, graph));
    17.8 +    (Symtab.curried_update (name, info) theories, files, tex_index, html_index, graph));
    17.9  
   17.10  fun change_theory_info name f =
   17.11    change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
   17.12 -    (case Symtab.lookup (theories, name) of
   17.13 +    (case Symtab.curried_lookup theories name of
   17.14        NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info)
   17.15 -    | SOME info => (Symtab.update ((name, map_theory_info f info), theories), files,
   17.16 +    | SOME info => (Symtab.curried_update (name, map_theory_info f info) theories, files,
   17.17          tex_index, html_index, graph)));
   17.18  
   17.19  
    18.1 --- a/src/Pure/Thy/thm_database.ML	Thu Sep 01 16:19:02 2005 +0200
    18.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Sep 01 18:48:50 2005 +0200
    18.3 @@ -88,7 +88,7 @@
    18.4          fun result prfx bname =
    18.5            if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
    18.6                NameSpace.intern space xname = name then
    18.7 -            SOME (prfx, (bname, xname, length (the (Symtab.lookup (thms, name))) = 1))
    18.8 +            SOME (prfx, (bname, xname, length (the (Symtab.curried_lookup thms name)) = 1))
    18.9            else NONE;
   18.10          val names = NameSpace.unpack name;
   18.11        in
    19.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Sep 01 16:19:02 2005 +0200
    19.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Sep 01 18:48:50 2005 +0200
    19.3 @@ -469,7 +469,7 @@
    19.4    end;
    19.5  
    19.6  fun sect tab ((Keyword, s, n) :: toks) =
    19.7 -      (case Symtab.lookup (tab, s) of
    19.8 +      (case Symtab.curried_lookup tab s of
    19.9          SOME parse => !! parse toks
   19.10        | NONE => syn_err "section" s n)
   19.11    | sect _ ((_, s, n) :: _) = syn_err "section" s n
    20.1 --- a/src/Pure/axclass.ML	Thu Sep 01 16:19:02 2005 +0200
    20.2 +++ b/src/Pure/axclass.ML	Thu Sep 01 18:48:50 2005 +0200
    20.3 @@ -153,7 +153,7 @@
    20.4  
    20.5  (* get and put data *)
    20.6  
    20.7 -fun lookup_axclass_info thy c = Symtab.lookup (AxclassesData.get thy, c);
    20.8 +val lookup_axclass_info = Symtab.curried_lookup o AxclassesData.get;
    20.9  
   20.10  fun get_axclass_info thy c =
   20.11    (case lookup_axclass_info thy c of
   20.12 @@ -161,7 +161,7 @@
   20.13    | SOME info => info);
   20.14  
   20.15  fun put_axclass_info c info thy =
   20.16 -  thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy));
   20.17 +  thy |> AxclassesData.put (Symtab.curried_update (c, info) (AxclassesData.get thy));
   20.18  
   20.19  
   20.20  (* class_axms *)
    21.1 --- a/src/Pure/compress.ML	Thu Sep 01 16:19:02 2005 +0200
    21.2 +++ b/src/Pure/compress.ML	Thu Sep 01 18:48:50 2005 +0200
    21.3 @@ -42,11 +42,11 @@
    21.4    let
    21.5      val typs = #1 (CompressData.get thy);
    21.6      fun compress T =
    21.7 -      (case Typtab.lookup (! typs, T) of
    21.8 +      (case Typtab.curried_lookup (! typs) T of
    21.9          SOME T' => T'
   21.10        | NONE =>
   21.11            let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
   21.12 -          in change typs (curry Typtab.update (T', T')); T' end);
   21.13 +          in change typs (Typtab.curried_update (T', T')); T' end);
   21.14    in compress end;
   21.15  
   21.16  
   21.17 @@ -58,9 +58,9 @@
   21.18      fun compress (t $ u) = compress t $ compress u
   21.19        | compress (Abs (a, T, t)) = Abs (a, T, compress t)
   21.20        | compress t =
   21.21 -          (case Termtab.lookup (! terms, t) of
   21.22 +          (case Termtab.curried_lookup (! terms) t of
   21.23              SOME t' => t'
   21.24 -          | NONE => (change terms (curry Termtab.update (t, t)); t));
   21.25 +          | NONE => (change terms (Termtab.curried_update (t, t)); t));
   21.26    in compress o map_term_types (typ thy) end;
   21.27  
   21.28  end;
    22.1 --- a/src/Pure/context.ML	Thu Sep 01 16:19:02 2005 +0200
    22.2 +++ b/src/Pure/context.ML	Thu Sep 01 18:48:50 2005 +0200
    22.3 @@ -121,7 +121,7 @@
    22.4  val kinds = ref (Inttab.empty: kind Inttab.table);
    22.5  
    22.6  fun invoke meth_name meth_fn k =
    22.7 -  (case Inttab.lookup (! kinds, k) of
    22.8 +  (case Inttab.curried_lookup (! kinds) k of
    22.9      SOME kind => meth_fn kind |> transform_failure (fn exn =>
   22.10        DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   22.11    | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
   22.12 @@ -140,7 +140,7 @@
   22.13      val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
   22.14      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   22.15        warning ("Duplicate declaration of theory data " ^ quote name));
   22.16 -    val _ = kinds := Inttab.update ((k, kind), ! kinds);
   22.17 +    val _ = change kinds (Inttab.curried_update (k, kind));
   22.18    in k end;
   22.19  
   22.20  val copy_data = Inttab.map' invoke_copy;
   22.21 @@ -256,7 +256,7 @@
   22.22    if draft_id id orelse Inttab.defined ids (#1 id) then ids
   22.23    else if Inttab.exists (equal (#2 id) o #2) ids then
   22.24      raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
   22.25 -  else Inttab.update (id, ids);
   22.26 +  else Inttab.curried_update id ids;
   22.27  
   22.28  fun check_insert intermediate id (ids, iids) =
   22.29    let val ids' = check_ins id ids and iids' = check_ins id iids
   22.30 @@ -423,12 +423,12 @@
   22.31  val declare = declare_theory_data;
   22.32  
   22.33  fun get k dest thy =
   22.34 -  (case Inttab.lookup (#theory (data_of thy), k) of
   22.35 +  (case Inttab.curried_lookup (#theory (data_of thy)) k of
   22.36      SOME x => (dest x handle Match =>
   22.37        error ("Failed to access theory data " ^ quote (invoke_name k)))
   22.38    | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
   22.39  
   22.40 -fun put k mk x = modify_thy (map_theory (curry Inttab.update (k, mk x)));
   22.41 +fun put k mk x = modify_thy (map_theory (Inttab.curried_update (k, mk x)));
   22.42  fun init k = put k I (invoke_empty k);
   22.43  
   22.44  end;
   22.45 @@ -525,7 +525,7 @@
   22.46  val kinds = ref (Inttab.empty: kind Inttab.table);
   22.47  
   22.48  fun invoke meth_name meth_fn k =
   22.49 -  (case Inttab.lookup (! kinds, k) of
   22.50 +  (case Inttab.curried_lookup (! kinds) k of
   22.51      SOME kind => meth_fn kind |> transform_failure (fn exn =>
   22.52        DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   22.53    | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   22.54 @@ -549,18 +549,18 @@
   22.55      val kind = {name = name, init = init};
   22.56      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   22.57        warning ("Duplicate declaration of proof data " ^ quote name));
   22.58 -    val _ = kinds := Inttab.update ((k, kind), ! kinds);
   22.59 +    val _ = change kinds (Inttab.curried_update (k, kind));
   22.60    in k end;
   22.61  
   22.62 -fun init k = modify_thy (map_proof (curry Inttab.update (k, ())));
   22.63 +fun init k = modify_thy (map_proof (Inttab.curried_update (k, ())));
   22.64  
   22.65  fun get k dest prf =
   22.66 -  (case Inttab.lookup (data_of_proof prf, k) of
   22.67 +  (case Inttab.curried_lookup (data_of_proof prf) k of
   22.68      SOME x => (dest x handle Match =>
   22.69        error ("Failed to access proof data " ^ quote (invoke_name k)))
   22.70    | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
   22.71  
   22.72 -fun put k mk x = map_prf (curry Inttab.update (k, mk x));
   22.73 +fun put k mk x = map_prf (Inttab.curried_update (k, mk x));
   22.74  
   22.75  end;
   22.76  
    23.1 --- a/src/Pure/fact_index.ML	Thu Sep 01 16:19:02 2005 +0200
    23.2 +++ b/src/Pure/fact_index.ML	Thu Sep 01 18:48:50 2005 +0200
    23.3 @@ -55,7 +55,7 @@
    23.4  
    23.5  fun add pred (name, ths) (Index {next, facts, consts, frees}) =
    23.6    let
    23.7 -    fun upd a tab = Symtab.update_multi ((a, (next, (name, ths))), tab);
    23.8 +    fun upd a = Symtab.curried_update_multi (a, (next, (name, ths)));
    23.9      val (cs, xs) = fold (index_thm pred) ths ([], []);
   23.10    in
   23.11      Index {next = next + 1, facts = (name, ths) :: facts,
   23.12 @@ -74,7 +74,7 @@
   23.13  
   23.14  fun find idx ([], []) = facts idx
   23.15    | find (Index {consts, frees, ...}) (cs, xs) =
   23.16 -      (map (curry Symtab.lookup_multi consts) cs @
   23.17 -        map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
   23.18 +      (map (Symtab.curried_lookup_multi consts) cs @
   23.19 +        map (Symtab.curried_lookup_multi frees) xs) |> intersects |> map #2;
   23.20  
   23.21  end;
    24.1 --- a/src/Pure/net.ML	Thu Sep 01 16:19:02 2005 +0200
    24.2 +++ b/src/Pure/net.ML	Thu Sep 01 18:48:50 2005 +0200
    24.3 @@ -94,8 +94,8 @@
    24.4              Net{comb=comb, var=ins1(keys,var), atoms=atoms}
    24.5          | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
    24.6              let
    24.7 -              val net' = if_none (Symtab.lookup (atoms, a)) empty;
    24.8 -              val atoms' = Symtab.update ((a, ins1(keys,net')), atoms);
    24.9 +              val net' = if_none (Symtab.curried_lookup atoms a) empty;
   24.10 +              val atoms' = Symtab.curried_update (a, ins1 (keys, net')) atoms;
   24.11              in  Net{comb=comb, var=var, atoms=atoms'}  end
   24.12    in  ins1 (keys,net)  end;
   24.13  
   24.14 @@ -126,12 +126,12 @@
   24.15              newnet{comb=comb, var=del1(keys,var), atoms=atoms}
   24.16          | del1 (AtomK a :: keys, Net{comb,var,atoms}) =
   24.17              let val atoms' =
   24.18 -              (case Symtab.lookup (atoms, a) of
   24.19 +              (case Symtab.curried_lookup atoms a of
   24.20                  NONE => raise DELETE
   24.21                | SOME net' =>
   24.22                    (case del1 (keys, net') of
   24.23                      Leaf [] => Symtab.delete a atoms
   24.24 -                  | net'' => Symtab.update ((a, net''), atoms)))
   24.25 +                  | net'' => Symtab.curried_update (a, net'') atoms))
   24.26              in  newnet{comb=comb, var=var, atoms=atoms'}  end
   24.27    in  del1 (keys,net)  end;
   24.28  
   24.29 @@ -143,7 +143,7 @@
   24.30  exception ABSENT;
   24.31  
   24.32  fun the_atom atoms a =
   24.33 -  (case Symtab.lookup (atoms, a) of
   24.34 +  (case Symtab.curried_lookup atoms a of
   24.35      NONE => raise ABSENT
   24.36    | SOME net => net);
   24.37  
   24.38 @@ -222,7 +222,7 @@
   24.39            subtr comb1 comb2
   24.40            #> subtr var1 var2
   24.41            #> Symtab.fold (fn (a, net) =>
   24.42 -            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2
   24.43 +            subtr (if_none (Symtab.curried_lookup atoms1 a) emptynet) net) atoms2
   24.44    in subtr net1 net2 [] end;
   24.45  
   24.46  fun entries net = subtract (K false) empty net;
    25.1 --- a/src/Pure/pattern.ML	Thu Sep 01 16:19:02 2005 +0200
    25.2 +++ b/src/Pure/pattern.ML	Thu Sep 01 18:48:50 2005 +0200
    25.3 @@ -357,7 +357,7 @@
    25.4            if loose_bvar(t,0) then raise MATCH
    25.5            else (case Envir.lookup' (insts, (ixn, T)) of
    25.6                    NONE => (typ_match thy (tyinsts, (T, fastype_of t)),
    25.7 -                           Vartab.update_new ((ixn, (T, t)), insts))
    25.8 +                           Vartab.curried_update_new (ixn, (T, t)) insts)
    25.9                  | SOME u => if t aeconv u then instsp else raise MATCH)
   25.10        | (Free (a,T), Free (b,U)) =>
   25.11            if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
   25.12 @@ -378,11 +378,11 @@
   25.13  fun match_bind(itms,binders,ixn,T,is,t) =
   25.14    let val js = loose_bnos t
   25.15    in if null is
   25.16 -     then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH
   25.17 +     then if null js then Vartab.curried_update_new (ixn, (T, t)) itms else raise MATCH
   25.18       else if js subset_int is
   25.19            then let val t' = if downto0(is,length binders - 1) then t
   25.20                              else mapbnd (idx is) t
   25.21 -               in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end
   25.22 +               in Vartab.curried_update_new (ixn, (T, mkabs (binders, is, t'))) itms end
   25.23            else raise MATCH
   25.24    end;
   25.25  
    26.1 --- a/src/Pure/proof_general.ML	Thu Sep 01 16:19:02 2005 +0200
    26.2 +++ b/src/Pure/proof_general.ML	Thu Sep 01 18:48:50 2005 +0200
    26.3 @@ -811,11 +811,11 @@
    26.4  
    26.5      fun get_keywords_classification_table () =
    26.6          case (!keywords_classification_table) of
    26.7 -            SOME t => t
    26.8 -          | NONE => (let
    26.9 -                         val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab))
   26.10 -                                         (Symtab.empty,OuterSyntax.dest_parsers())
   26.11 -                     in (keywords_classification_table := SOME tab; tab) end)
   26.12 +          SOME t => t
   26.13 +        | NONE => (let
   26.14 +                     val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k))
   26.15 +                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
   26.16 +                   in (keywords_classification_table := SOME tab; tab) end)
   26.17  
   26.18  
   26.19  
   26.20 @@ -959,7 +959,7 @@
   26.21  
   26.22  fun xmls_of_transition (name,str,toks) =
   26.23     let
   26.24 -       val classification = Symtab.lookup (get_keywords_classification_table(),name)
   26.25 +     val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name
   26.26     in case classification of
   26.27            SOME k => (xmls_of_kind k (name,toks,str))
   26.28          | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
    27.1 --- a/src/Pure/proofterm.ML	Thu Sep 01 16:19:02 2005 +0200
    27.2 +++ b/src/Pure/proofterm.ML	Thu Sep 01 18:48:50 2005 +0200
    27.3 @@ -143,10 +143,10 @@
    27.4        | oras_of (prf % _) = oras_of prf
    27.5        | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
    27.6        | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
    27.7 -          case Symtab.lookup (thms, name) of
    27.8 -            NONE => oras_of prf (Symtab.update ((name, [prop]), thms), oras)
    27.9 +          case Symtab.curried_lookup thms name of
   27.10 +            NONE => oras_of prf (Symtab.curried_update (name, [prop]) thms, oras)
   27.11            | SOME ps => if prop mem ps then tabs else
   27.12 -              oras_of prf (Symtab.update ((name, prop::ps), thms), oras))
   27.13 +              oras_of prf (Symtab.curried_update (name, prop::ps) thms, oras))
   27.14        | oras_of (Oracle (s, prop, _)) =
   27.15            apsnd (OrdList.insert string_term_ord (s, prop))
   27.16        | oras_of (MinProof (thms, _, oras)) =
   27.17 @@ -162,10 +162,10 @@
   27.18    | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
   27.19    | thms_of_proof (prf % _) = thms_of_proof prf
   27.20    | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
   27.21 -      case Symtab.lookup (tab, s) of
   27.22 -        NONE => thms_of_proof prf (Symtab.update ((s, [(prop, prf')]), tab))
   27.23 +      case Symtab.curried_lookup tab s of
   27.24 +        NONE => thms_of_proof prf (Symtab.curried_update (s, [(prop, prf')]) tab)
   27.25        | SOME ps => if exists (equal prop o fst) ps then tab else
   27.26 -          thms_of_proof prf (Symtab.update ((s, (prop, prf')::ps), tab)))
   27.27 +          thms_of_proof prf (Symtab.curried_update (s, (prop, prf')::ps) tab))
   27.28    | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
   27.29    | thms_of_proof _ = I;
   27.30  
   27.31 @@ -173,7 +173,7 @@
   27.32    | axms_of_proof (AbsP (_, _, prf)) = axms_of_proof prf
   27.33    | axms_of_proof (prf1 %% prf2) = axms_of_proof prf1 #> axms_of_proof prf2
   27.34    | axms_of_proof (prf % _) = axms_of_proof prf
   27.35 -  | axms_of_proof (prf as PAxm (s, _, _)) = curry Symtab.update (s, prf)
   27.36 +  | axms_of_proof (prf as PAxm (s, _, _)) = Symtab.curried_update (s, prf)
   27.37    | axms_of_proof (MinProof (_, prfs, _)) = fold (axms_of_proof o proof_of_min_axm) prfs
   27.38    | axms_of_proof _ = I;
   27.39  
    28.1 --- a/src/Pure/pure_thy.ML	Thu Sep 01 16:19:02 2005 +0200
    28.2 +++ b/src/Pure/pure_thy.ML	Thu Sep 01 18:48:50 2005 +0200
    28.3 @@ -208,8 +208,8 @@
    28.4      val (space, thms) = #theorems (get_theorems thy);
    28.5    in
    28.6      fn name =>
    28.7 -      Option.map (map (Thm.transfer (Theory.deref thy_ref)))    (*dynamic identity*)
    28.8 -      (Symtab.lookup (thms, NameSpace.intern space name))       (*static content*)
    28.9 +      Option.map (map (Thm.transfer (Theory.deref thy_ref)))     (*dynamic identity*)
   28.10 +      (Symtab.curried_lookup thms (NameSpace.intern space name)) (*static content*)
   28.11    end;
   28.12  
   28.13  fun get_thms_closure thy =
   28.14 @@ -309,10 +309,10 @@
   28.15          val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
   28.16          val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy';
   28.17          val space' = Sign.declare_name thy' name space;
   28.18 -        val theorems' = Symtab.update ((name, thms'), theorems);
   28.19 +        val theorems' = Symtab.curried_update (name, thms') theorems;
   28.20          val index' = FactIndex.add (K false) (name, thms') index;
   28.21        in
   28.22 -        (case Symtab.lookup (theorems, name) of
   28.23 +        (case Symtab.curried_lookup theorems name of
   28.24            NONE => ()
   28.25          | SOME thms'' =>
   28.26              if Thm.eq_thms (thms', thms'') then warn_same name
    29.1 --- a/src/Pure/sign.ML	Thu Sep 01 16:19:02 2005 +0200
    29.2 +++ b/src/Pure/sign.ML	Thu Sep 01 18:48:50 2005 +0200
    29.3 @@ -282,8 +282,8 @@
    29.4  
    29.5  fun const_constraint thy c =
    29.6    let val ((_, consts), constraints) = #consts (rep_sg thy) in
    29.7 -    (case Symtab.lookup (constraints, c) of
    29.8 -      NONE => Option.map #1 (Symtab.lookup (consts, c))
    29.9 +    (case Symtab.curried_lookup constraints c of
   29.10 +      NONE => Option.map #1 (Symtab.curried_lookup consts c)
   29.11      | some => some)
   29.12    end;
   29.13  
   29.14 @@ -291,7 +291,7 @@
   29.15    (case const_constraint thy c of SOME T => T
   29.16    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   29.17  
   29.18 -fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
   29.19 +val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg);
   29.20  
   29.21  fun the_const_type thy c =
   29.22    (case const_type thy c of SOME T => T
   29.23 @@ -514,7 +514,7 @@
   29.24  
   29.25  fun read_tyname thy raw_c =
   29.26    let val c = intern_type thy raw_c in
   29.27 -    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c) of
   29.28 +    (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
   29.29        SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
   29.30      | _ => error ("Undeclared type constructor: " ^ quote c))
   29.31    end;
   29.32 @@ -714,7 +714,7 @@
   29.33        handle TYPE (msg, _, _) => error msg;
   29.34      val _ = cert_term thy (Const (c, T))
   29.35        handle TYPE (msg, _, _) => error msg;
   29.36 -  in thy |> map_consts (apsnd (curry Symtab.update (c, T))) end;
   29.37 +  in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end;
   29.38  
   29.39  val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
   29.40  val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
    30.1 --- a/src/Pure/sorts.ML	Thu Sep 01 16:19:02 2005 +0200
    30.2 +++ b/src/Pure/sorts.ML	Thu Sep 01 18:48:50 2005 +0200
    30.3 @@ -180,7 +180,7 @@
    30.4  fun mg_domain (classes, arities) a S =
    30.5    let
    30.6      fun dom c =
    30.7 -      (case AList.lookup (op =) (Symtab.lookup_multi (arities, a)) c of
    30.8 +      (case AList.lookup (op =) (Symtab.curried_lookup_multi arities a) c of
    30.9          NONE => raise DOMAIN (a, c)
   30.10        | SOME Ss => Ss);
   30.11      fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
    31.1 --- a/src/Pure/thm.ML	Thu Sep 01 16:19:02 2005 +0200
    31.2 +++ b/src/Pure/thm.ML	Thu Sep 01 18:48:50 2005 +0200
    31.3 @@ -524,7 +524,7 @@
    31.4  fun get_axiom_i theory name =
    31.5    let
    31.6      fun get_ax thy =
    31.7 -      Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name)
    31.8 +      Symtab.curried_lookup (#2 (#axioms (Theory.rep_theory thy))) name
    31.9        |> Option.map (fn prop =>
   31.10            Thm {thy_ref = Theory.self_ref thy,
   31.11              der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
   31.12 @@ -1482,7 +1482,7 @@
   31.13  fun invoke_oracle_i thy1 name =
   31.14    let
   31.15      val oracle =
   31.16 -      (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1)), name) of
   31.17 +      (case Symtab.curried_lookup (#2 (#oracles (Theory.rep_theory thy1))) name of
   31.18          NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
   31.19        | SOME (f, _) => f);
   31.20      val thy_ref1 = Theory.self_ref thy1;
    32.1 --- a/src/Pure/type.ML	Thu Sep 01 16:19:02 2005 +0200
    32.2 +++ b/src/Pure/type.ML	Thu Sep 01 18:48:50 2005 +0200
    32.3 @@ -167,7 +167,7 @@
    32.4              val Ts' = map cert Ts;
    32.5              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    32.6            in
    32.7 -            (case Symtab.lookup (types, c) of
    32.8 +            (case Symtab.curried_lookup types c of
    32.9                SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
   32.10              | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
   32.11                  if syn then check_syntax c else ();
   32.12 @@ -284,7 +284,7 @@
   32.13    [TVar (ixn, S), TVar (ixn, S')], []);
   32.14  
   32.15  fun lookup (tye, (ixn, S)) =
   32.16 -  (case Vartab.lookup (tye, ixn) of
   32.17 +  (case Vartab.curried_lookup tye ixn of
   32.18      NONE => NONE
   32.19    | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
   32.20  
   32.21 @@ -298,7 +298,7 @@
   32.22      fun match (TVar (v, S), T) subs =
   32.23            (case lookup (subs, (v, S)) of
   32.24              NONE =>
   32.25 -              if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs)
   32.26 +              if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs
   32.27                else raise TYPE_MATCH
   32.28            | SOME U => if U = T then subs else raise TYPE_MATCH)
   32.29        | match (Type (a, Ts), Type (b, Us)) subs =
   32.30 @@ -317,7 +317,7 @@
   32.31  (*purely structural matching*)
   32.32  fun raw_match (TVar (v, S), T) subs =
   32.33        (case lookup (subs, (v, S)) of
   32.34 -        NONE => Vartab.update_new ((v, (S, T)), subs)
   32.35 +        NONE => Vartab.curried_update_new (v, (S, T)) subs
   32.36        | SOME U => if U = T then subs else raise TYPE_MATCH)
   32.37    | raw_match (Type (a, Ts), Type (b, Us)) subs =
   32.38        if a <> b then raise TYPE_MATCH
   32.39 @@ -366,8 +366,8 @@
   32.40      fun meet (_, []) tye = tye
   32.41        | meet (TVar (xi, S'), S) tye =
   32.42            if Sorts.sort_le classes (S', S) then tye
   32.43 -          else Vartab.update_new ((xi, (S',
   32.44 -            gen_tyvar (Sorts.inter_sort classes (S', S)))), tye)
   32.45 +          else Vartab.curried_update_new
   32.46 +            (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye
   32.47        | meet (TFree (_, S'), S) tye =
   32.48            if Sorts.sort_le classes (S', S) then tye
   32.49            else raise TUNIFY
   32.50 @@ -381,19 +381,19 @@
   32.51            if eq_ix (v, w) then
   32.52              if S1 = S2 then tye else tvar_clash v S1 S2
   32.53            else if Sorts.sort_le classes (S1, S2) then
   32.54 -            Vartab.update_new ((w, (S2, T)), tye)
   32.55 +            Vartab.curried_update_new (w, (S2, T)) tye
   32.56            else if Sorts.sort_le classes (S2, S1) then
   32.57 -            Vartab.update_new ((v, (S1, U)), tye)
   32.58 +            Vartab.curried_update_new (v, (S1, U)) tye
   32.59            else
   32.60              let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
   32.61 -              Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye))
   32.62 +              Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye)
   32.63              end
   32.64        | (TVar (v, S), T) =>
   32.65            if occurs v tye T then raise TUNIFY
   32.66 -          else meet (T, S) (Vartab.update_new ((v, (S, T)), tye))
   32.67 +          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
   32.68        | (T, TVar (v, S)) =>
   32.69            if occurs v tye T then raise TUNIFY
   32.70 -          else meet (T, S) (Vartab.update_new ((v, (S, T)), tye))
   32.71 +          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
   32.72        | (Type (a, Ts), Type (b, Us)) =>
   32.73            if a <> b then raise TUNIFY
   32.74            else unifs (Ts, Us) tye
   32.75 @@ -408,13 +408,13 @@
   32.76      (T as TVar (v, S1), U as TVar (w, S2)) =>
   32.77        if eq_ix (v, w) then
   32.78          if S1 = S2 then tye else tvar_clash v S1 S2
   32.79 -      else Vartab.update_new ((w, (S2, T)), tye)
   32.80 +      else Vartab.curried_update_new (w, (S2, T)) tye
   32.81    | (TVar (v, S), T) =>
   32.82        if occurs v tye T then raise TUNIFY
   32.83 -      else Vartab.update_new ((v, (S, T)), tye)
   32.84 +      else Vartab.curried_update_new (v, (S, T)) tye
   32.85    | (T, TVar (v, S)) =>
   32.86        if occurs v tye T then raise TUNIFY
   32.87 -      else Vartab.update_new ((v, (S, T)), tye)
   32.88 +      else Vartab.curried_update_new (v, (S, T)) tye
   32.89    | (Type (a, Ts), Type (b, Us)) =>
   32.90        if a <> b then raise TUNIFY
   32.91        else raw_unifys (Ts, Us) tye
   32.92 @@ -476,9 +476,9 @@
   32.93  
   32.94  fun insert_arities pp classes (t, ars) arities =
   32.95    let val ars' =
   32.96 -    Symtab.lookup_multi (arities, t)
   32.97 +    Symtab.curried_lookup_multi arities t
   32.98      |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   32.99 -  in Symtab.update ((t, ars'), arities) end;
  32.100 +  in Symtab.curried_update (t, ars') arities end;
  32.101  
  32.102  fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
  32.103    insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
  32.104 @@ -488,7 +488,7 @@
  32.105  fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
  32.106    let
  32.107      fun prep (t, Ss, S) =
  32.108 -      (case Symtab.lookup (#2 types, t) of
  32.109 +      (case Symtab.curried_lookup (#2 types) t of
  32.110          SOME (LogicalType n, _) =>
  32.111            if length Ss = n then
  32.112              (t, map (cert_sort tsig) Ss, cert_sort tsig S)
  32.113 @@ -591,18 +591,18 @@
  32.114      val c' = NameSpace.full naming c;
  32.115      val space' = NameSpace.declare naming c' space;
  32.116      val types' =
  32.117 -      (case Symtab.lookup (types, c') of
  32.118 +      (case Symtab.curried_lookup types c' of
  32.119          SOME (decl', _) => err_in_decls c' decl decl'
  32.120 -      | NONE => Symtab.update ((c', (decl, stamp ())), types));
  32.121 +      | NONE => Symtab.curried_update (c', (decl, stamp ())) types);
  32.122    in (space', types') end;
  32.123  
  32.124 -fun the_decl (_, types) c = fst (the (Symtab.lookup (types, c)));
  32.125 +fun the_decl (_, types) = fst o the o Symtab.curried_lookup types;
  32.126  
  32.127  fun change_types f = map_tsig (fn (classes, default, types, arities) =>
  32.128    (classes, default, f types, arities));
  32.129  
  32.130  fun syntactic types (Type (c, Ts)) =
  32.131 -      (case Symtab.lookup (types, c) of SOME (Nonterminal, _) => true | _ => false)
  32.132 +      (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false)
  32.133          orelse exists (syntactic types) Ts
  32.134    | syntactic _ _ = false;
  32.135