curried_lookup/update;
tuned;

--- a/src/Provers/Arith/cancel_numerals.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -11,7 +11,7 @@
 
 It works by (a) massaging both sides to bring the selected term to the front:
 
-     #m*u + (i + j) ~~ #m'*u + (i' + j') 
+     #m*u + (i + j) ~~ #m'*u + (i' + j')
 
 (b) then using bal_add1 or bal_add2 to reach
 
@@ -36,7 +36,7 @@
   val bal_add1: thm
   val bal_add2: thm
   (*proof tools*)
-  val prove_conv: tactic list -> theory -> 
+  val prove_conv: tactic list -> theory ->
                   thm list -> string list -> term * term -> thm option
   val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
@@ -48,24 +48,22 @@
 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
   sig
   val proc: theory -> simpset -> term -> thm option
-  end 
+  end
 =
 struct
 
 (*For t = #n*u then put u in the table*)
-fun update_by_coeff (tab, t) =
-  Termtab.update ((#2 (Data.dest_coeff t), ()), tab);
+fun update_by_coeff t =
+  Termtab.curried_update (#2 (Data.dest_coeff t), ());
 
 (*a left-to-right scan of terms1, seeking a term of the form #n*u, where
   #m*u is in terms2 for some m*)
 fun find_common (terms1,terms2) =
-  let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
-      fun seek [] = raise TERM("find_common", []) 
-	| seek (t::terms) =
-	      let val (_,u) = Data.dest_coeff t 
-	      in  if isSome (Termtab.lookup (tab2, u)) then u
-		  else seek terms
-	      end
+  let val tab2 = fold update_by_coeff terms2 Termtab.empty
+      fun seek [] = raise TERM("find_common", [])
+        | seek (t::terms) =
+              let val (_,u) = Data.dest_coeff t
+              in if Termtab.defined tab2 u then u else seek terms end
   in  seek terms1 end;
 
 (*the simplification procedure*)
@@ -74,7 +72,7 @@
       val hyps = prems_of_ss ss;
       (*first freeze any Vars in the term to prevent flex-flex problems*)
       val (t', xs) = Term.adhoc_freeze_vars t;
-      val (t1,t2) = Data.dest_bal t' 
+      val (t1,t2) = Data.dest_bal t'
       val terms1 = Data.dest_sum t1
       and terms2 = Data.dest_sum t2
       val u = find_common (terms1,terms2)
@@ -83,30 +81,30 @@
       and T = Term.fastype_of u
       fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
       val reshape =  (*Move i*u to the front and put j*u into standard form
-		       i + #m + j + k == #m + i + (j + k) *)
-	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
-		raise TERM("cancel_numerals", []) 
-	    else Data.prove_conv [Data.norm_tac ss] thy hyps xs
-			(t', 
-			 Data.mk_bal (newshape(n1,terms1'), 
-				      newshape(n2,terms2')))
+                       i + #m + j + k == #m + i + (j + k) *)
+            if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
+                raise TERM("cancel_numerals", [])
+            else Data.prove_conv [Data.norm_tac ss] thy hyps xs
+                        (t',
+                         Data.mk_bal (newshape(n1,terms1'),
+                                      newshape(n2,terms2')))
   in
       Option.map (Data.simplify_meta_eq ss)
-       (if n2<=n1 then 
-	    Data.prove_conv 
-	       [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
-		Data.numeral_simp_tac ss] thy hyps xs
-	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
-				 Data.mk_sum T terms2'))
-	else
-	    Data.prove_conv 
-	       [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
-		Data.numeral_simp_tac ss] thy hyps xs
-	       (t', Data.mk_bal (Data.mk_sum T terms1', 
-				 newshape(n2-n1,terms2'))))
+       (if n2<=n1 then
+            Data.prove_conv
+               [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
+                Data.numeral_simp_tac ss] thy hyps xs
+               (t', Data.mk_bal (newshape(n1-n2,terms1'),
+                                 Data.mk_sum T terms2'))
+        else
+            Data.prove_conv
+               [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
+                Data.numeral_simp_tac ss] thy hyps xs
+               (t', Data.mk_bal (Data.mk_sum T terms1',
+                                 newshape(n2-n1,terms2'))))
   end
   handle TERM _ => NONE
        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
-			     Undeclared type constructor "Numeral.bin"*)
+                             Undeclared type constructor "Numeral.bin"*)
 
 end;

--- a/src/Provers/Arith/extract_common_term.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -37,12 +37,9 @@
 =
 struct
 
-(*Store the term t in the table*)
-fun update_by_coeff t tab = Termtab.update ((t, ()), tab);
-
 (*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
 fun find_common (terms1,terms2) =
-  let val tab2 = fold update_by_coeff terms2 Termtab.empty
+  let val tab2 = fold (Termtab.curried_update o rpair ()) terms2 Termtab.empty
       fun seek [] = raise TERM("find_common", []) 
 	| seek (u::terms) =
 	      if Termtab.defined tab2 u then u

--- a/src/Pure/Proof/extraction.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -301,8 +301,7 @@
   in
     ExtractionData.put
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
-       realizers = foldr Symtab.update_multi
-         realizers (map (prep_rlz thy) (rev rs)),
+       realizers = fold (Symtab.curried_update_multi o prep_rlz thy) rs realizers,
        defs = defs, expand = expand, prep = prep} thy
   end
 
@@ -565,7 +564,7 @@
               else fst (extr d defs vs ts Ts hs prf0)
           in
             if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
-            else case Symtab.lookup (realizers, name) of
+            else case Symtab.curried_lookup realizers name of
               NONE => (case find vs' (find' name defs') of
                 NONE =>
                   let
@@ -601,7 +600,7 @@
           in
             if etype_of thy' vs' [] prop = nullT andalso
               realizes_null vs' prop aconv prop then (defs, prf0)
-            else case find vs' (Symtab.lookup_multi (realizers, s)) of
+            else case find vs' (Symtab.curried_lookup_multi realizers s) of
               SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
             | NONE => error ("corr: no realizer for instance of axiom " ^
                 quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
@@ -649,7 +648,7 @@
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
           in
-            case Symtab.lookup (realizers, s) of
+            case Symtab.curried_lookup realizers s of
               NONE => (case find vs' (find' s defs) of
                 NONE =>
                   let
@@ -708,7 +707,7 @@
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
           in
-            case find vs' (Symtab.lookup_multi (realizers, s)) of
+            case find vs' (Symtab.curried_lookup_multi realizers s) of
               SOME (t, _) => (defs, subst_TVars tye' t)
             | NONE => error ("extr: no realizer for instance of axiom " ^
                 quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm

--- a/src/Pure/Proof/proof_syntax.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -97,10 +97,10 @@
     val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
 
     val tab = Symtab.foldl (fn (tab, (key, ps)) =>
-      let val prop = getOpt (assoc_string (thms', key), Bound 0)
+      let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0)
       in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
         if prop <> prop' then
-          (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
+          (Symtab.curried_update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
         else x) (tab, 1) ps)
       end) (Symtab.empty, thms);
 
@@ -110,8 +110,8 @@
       | rename (prf % t) = rename prf % t
       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
           let
-            val prop' = getOpt (assoc_string (thms', s), Bound 0);
-            val ps = map fst (valOf (Symtab.lookup (thms, s))) \ prop'
+            val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
+            val ps = map fst (the (Symtab.curried_lookup thms s)) \ prop'
           in if prop = prop' then prf' else
             PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
               prf, prop, Ts)
@@ -138,15 +138,15 @@
                "axm" :: xs =>
                  let
                    val name = NameSpace.pack xs;
-                   val prop = (case assoc_string (axms, name) of
+                   val prop = (case AList.lookup (op =) axms name of
                        SOME prop => prop
                      | NONE => error ("Unknown axiom " ^ quote name))
                  in PAxm (name, prop, NONE) end
              | "thm" :: xs =>
                  let val name = NameSpace.pack xs;
-                 in (case assoc_string (thms, name) of
+                 in (case AList.lookup (op =) thms name of
                      SOME thm => fst (strip_combt (Thm.proof_of thm))
-                   | NONE => (case Symtab.lookup (tab, name) of
+                   | NONE => (case Symtab.curried_lookup tab name of
                          SOME prf => prf
                        | NONE => error ("Unknown theorem " ^ quote name)))
                  end

--- a/src/Pure/Proof/proofchecker.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -19,9 +19,9 @@
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = fold_rev (curry Symtab.update) (PureThy.all_thms_of thy) Symtab.empty
+  let val tab = fold_rev Symtab.curried_update (PureThy.all_thms_of thy) Symtab.empty
   in
-    (fn s => case Symtab.lookup (tab, s) of
+    (fn s => case Symtab.curried_lookup tab s of
        NONE => error ("Unknown theorem " ^ quote s)
      | SOME thm => thm)
   end;

--- a/src/Pure/Tools/compute.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/Tools/compute.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -44,13 +44,13 @@
 val remove_types =
     let
         fun remove_types_var table invtable ccount vcount ldepth t =
-            (case Termtab.lookup (table, t) of
+            (case Termtab.curried_lookup table t of
                  NONE =>
                  let
                      val a = AbstractMachine.Var vcount
                  in
-                     (Termtab.update ((t, a), table),
-                      AMTermTab.update ((a, t), invtable),
+                     (Termtab.curried_update (t, a) table,
+                      AMTermTab.curried_update (a, t) invtable,
                       ccount,
                       inc vcount,
                       AbstractMachine.Var (add vcount ldepth))
@@ -60,13 +60,13 @@
                | SOME _ => sys_error "remove_types_var: lookup should be a var")
 
         fun remove_types_const table invtable ccount vcount ldepth t =
-            (case Termtab.lookup (table, t) of
+            (case Termtab.curried_lookup table t of
                  NONE =>
                  let
                      val a = AbstractMachine.Const ccount
                  in
-                     (Termtab.update ((t, a), table),
-                      AMTermTab.update ((a, t), invtable),
+                     (Termtab.curried_update (t, a) table,
+                      AMTermTab.curried_update (a, t) invtable,
                       inc ccount,
                       vcount,
                       a)
@@ -114,12 +114,12 @@
     let
         fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
             if v < ldepth then (Bound v, List.nth (bounds, v)) else
-            (case AMTermTab.lookup (invtable, AbstractMachine.Var (v-ldepth)) of
+            (case AMTermTab.curried_lookup invtable (AbstractMachine.Var (v-ldepth)) of
                  SOME (t as Var (_, ty)) => (t, ty)
                | SOME (t as Free (_, ty)) => (t, ty)
                | _ => sys_error "infer_types: lookup should deliver Var or Free")
           | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
-            (case AMTermTab.lookup (invtable, c) of
+            (case AMTermTab.curried_lookup invtable c of
                  SOME (c as Const (_, ty)) => (c, ty)
                | _ => sys_error "infer_types: lookup should deliver Const")
           | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
@@ -176,10 +176,10 @@
 
                 fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
                     let
-                        val var' = valOf (AMTermTab.lookup (invtable, var))
+                        val var' = valOf (AMTermTab.curried_lookup invtable var)
                         val table = Termtab.delete var' table
                         val invtable = AMTermTab.delete var invtable
-                        val vars = Inttab.update_new ((v, n), vars) handle Inttab.DUP _ =>
+                        val vars = Inttab.curried_update_new (v, n) vars handle Inttab.DUP _ =>
                           raise (Make "no duplicate variable in pattern allowed")
                     in
                         (table, invtable, n+1, vars, AbstractMachine.PVar)
@@ -217,7 +217,7 @@
 
                 fun rename ldepth vars (var as AbstractMachine.Var v) =
                     if v < ldepth then var
-                    else (case Inttab.lookup (vars, v-ldepth) of
+                    else (case Inttab.curried_lookup vars (v - ldepth) of
                               NONE => raise (Make "new variable on right hand side")
                             | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
                   | rename ldepth vars (c as AbstractMachine.Const _) = c
@@ -231,14 +231,12 @@
             end
 
         val (table, invtable, ccount, rules) =
-            List.foldl (fn (th, (table, invtable, ccount, rules)) =>
-                           let
-                               val (table, invtable, ccount, rule) =
-                                   thm2rule table invtable ccount th
-                           in
-                               (table, invtable, ccount, rule::rules)
-                           end)
-                       (Termtab.empty, AMTermTab.empty, 0, []) (List.rev ths)
+          fold_rev (fn th => fn (table, invtable, ccount, rules) =>
+            let
+              val (table, invtable, ccount, rule) =
+                  thm2rule table invtable ccount th
+            in (table, invtable, ccount, rule::rules) end)
+          ths (Termtab.empty, AMTermTab.empty, 0, [])
 
         val prog = AbstractMachine.compile rules
 

--- a/src/Pure/defs.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/defs.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -46,13 +46,13 @@
          typ  (* type of the constant in this particular definition *)
          * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
 
-fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
+fun getnode graph = the o Symtab.curried_lookup graph
 fun get_nodedefs (Node (_, defs, _, _, _)) = defs
-fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname)
-fun get_defnode' graph noderef defname =
-    Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
+fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.curried_lookup defs defname
+fun get_defnode' graph noderef =
+  Symtab.curried_lookup (get_nodedefs (the (Symtab.curried_lookup graph noderef)))
 
-fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
+fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0;
 
 datatype graphaction =
     Declare of string * typ
@@ -89,14 +89,14 @@
 fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
 
 fun subst_incr_tvar inc t =
-    if (inc > 0) then
+    if inc > 0 then
       let
         val tv = typ_tvars t
         val t' = Logic.incr_tvar inc t
-        fun update_subst (((n,i), _), s) =
-            Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
+        fun update_subst ((n, i), _) =
+          Vartab.curried_update ((n, i), ([], TVar ((n, i + inc), [])));
       in
-        (t',List.foldl update_subst Vartab.empty tv)
+        (t', fold update_subst tv Vartab.empty)
       end
     else
       (t, Vartab.empty)
@@ -157,9 +157,9 @@
             ((tab,max), []) ts
 
       fun idx (tab,max) (TVar ((a,i),_)) =
-          (case Inttab.lookup (tab, i) of
+          (case Inttab.curried_lookup tab i of
              SOME j => ((tab, max), TVar ((a,j),[]))
-           | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
+           | NONE => ((Inttab.curried_update (i, max) tab, max + 1), TVar ((a,max),[])))
         | idx (tab,max) (Type (t, ts)) =
           let
             val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
@@ -207,10 +207,10 @@
 
 fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
     (cost, axmap, (Declare cty)::actions,
-     Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
+     Symtab.curried_update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
     handle Symtab.DUP _ =>
            let
-             val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name))
+             val (Node (gty, _, _, _, _)) = the (Symtab.curried_lookup graph name)
            in
              if is_instance_r ty gty andalso is_instance_r gty ty then
                g
@@ -227,13 +227,13 @@
       val _ = axcounter := c+1
       val axname' = axname^"_"^(IntInf.toString c)
     in
-      (Symtab.update ((axname', axname), axmap), axname')
+      (Symtab.curried_update (axname', axname) axmap, axname')
     end
 
 fun translate_ex axmap x =
     let
       fun translate (ty, nodename, axname) =
-          (ty, nodename, the (Symtab.lookup (axmap, axname)))
+          (ty, nodename, the (Symtab.curried_lookup axmap axname))
     in
       case x of
         INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
@@ -243,7 +243,7 @@
 
 fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
     let
-      val mainnode  = (case Symtab.lookup (graph, mainref) of
+      val mainnode  = (case Symtab.curried_lookup graph mainref of
                          NONE => def_err ("constant "^mainref^" is not declared")
                        | SOME n => n)
       val (Node (gty, defs, backs, finals, _)) = mainnode
@@ -273,17 +273,16 @@
              let
                val links = map normalize_edge_idx links
              in
-               Symtab.update ((nodename,
-                               case Symtab.lookup (edges, nodename) of
+               Symtab.curried_update (nodename,
+                               case Symtab.curried_lookup edges nodename of
                                  NONE => links
-                               | SOME links' => merge_edges links' links),
-                              edges)
+                               | SOME links' => merge_edges links' links) edges
              end)
 
       fun make_edges ((bodyn, bodyty), edges) =
           let
             val bnode =
-                (case Symtab.lookup (graph, bodyn) of
+                (case Symtab.curried_lookup graph bodyn of
                    NONE => def_err "body of constant definition references undeclared constant"
                  | SOME x => x)
             val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
@@ -346,13 +345,13 @@
                         sys_error ("install_backrefs: closed node cannot be updated")
                       else ()
               val defnames =
-                  (case Symtab.lookup (backs, mainref) of
+                  (case Symtab.curried_lookup backs mainref of
                      NONE => Symtab.empty
                    | SOME s => s)
-              val defnames' = Symtab.update_new ((axname, ()), defnames)
-              val backs' = Symtab.update ((mainref,defnames'), backs)
+              val defnames' = Symtab.curried_update_new (axname, ()) defnames
+              val backs' = Symtab.curried_update (mainref, defnames') backs
             in
-              Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph)
+              Symtab.curried_update (noderef, Node (ty, defs, backs', finals, closed)) graph
             end
           else
             graph
@@ -365,8 +364,8 @@
           else if closed = Open andalso is_instance_r gty ty then Closed else closed
 
       val thisDefnode = Defnode (ty, edges)
-      val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new
-        ((axname, thisDefnode), defs), backs, finals, closed)), graph)
+      val graph = Symtab.curried_update (mainref, Node (gty, Symtab.curried_update_new
+        (axname, thisDefnode) defs, backs, finals, closed)) graph
 
       (* Now we have to check all backreferences to this node and inform them about
          the new defnode. In this section we also check for circularity. *)
@@ -378,8 +377,8 @@
                       getnode graph noderef
                   val _ = if closed = Final then sys_error "update_defs: closed node" else ()
                   val (Defnode (def_ty, defnode_edges)) =
-                      the (Symtab.lookup (nodedefs, defname))
-                  val edges = the (Symtab.lookup (defnode_edges, mainref))
+                      the (Symtab.curried_lookup nodedefs defname)
+                  val edges = the (Symtab.curried_lookup defnode_edges mainref)
                   val refclosed = ref false
 
                   (* the type of thisDefnode is ty *)
@@ -417,7 +416,7 @@
                   val defnames' = if edges' = [] then
                                     defnames
                                   else
-                                    Symtab.update ((defname, ()), defnames)
+                                    Symtab.curried_update (defname, ()) defnames
                 in
                   if changed then
                     let
@@ -425,16 +424,15 @@
                           if edges' = [] then
                             Symtab.delete mainref defnode_edges
                           else
-                            Symtab.update ((mainref, edges'), defnode_edges)
+                            Symtab.curried_update (mainref, edges') defnode_edges
                       val defnode' = Defnode (def_ty, defnode_edges')
-                      val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
+                      val nodedefs' = Symtab.curried_update (defname, defnode') nodedefs
                       val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
                                       andalso no_forwards nodedefs'
                                    then Final else closed
                       val graph' =
-                          Symtab.update
-                            ((noderef,
-                              Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph)
+                        Symtab.curried_update
+                          (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph
                     in
                       (defnames', graph')
                     end
@@ -449,7 +447,7 @@
               (backs, graph')
             else
               let
-                val backs' = Symtab.update_new ((noderef, defnames'), backs)
+                val backs' = Symtab.curried_update_new (noderef, defnames') backs
               in
                 (backs', graph')
               end
@@ -460,7 +458,7 @@
       (* If a Circular exception is thrown then we never reach this point. *)
       val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
       val closed = if closed = Closed andalso no_forwards defs then Final else closed
-      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph)
+      val graph = Symtab.curried_update (mainref, Node (gty, defs, backs, finals, closed)) graph
       val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
     in
       (cost+3, axmap, actions', graph)
@@ -484,7 +482,7 @@
     end
 
 fun finalize' (cost, axmap, history, graph) (noderef, ty) =
-    case Symtab.lookup (graph, noderef) of
+    case Symtab.curried_lookup graph noderef of
       NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
     | SOME (Node (nodety, defs, backs, finals, closed)) =>
       let
@@ -521,8 +519,7 @@
             val closed = if closed = Open andalso is_instance_r nodety ty then
                            Closed else
                          closed
-            val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)),
-                                       graph)
+            val graph = Symtab.curried_update (noderef, Node (nodety, defs, backs, finals, closed)) graph
 
             fun update_backref ((graph, backs), (backrefname, backdefnames)) =
                 let
@@ -535,7 +532,7 @@
                             the (get_defnode backnode backdefname)
 
                         val (defnames', all_edges') =
-                            case Symtab.lookup (all_edges, noderef) of
+                            case Symtab.curried_lookup all_edges noderef of
                               NONE => sys_error "finalize: corrupt backref"
                             | SOME edges =>
                               let
@@ -545,11 +542,11 @@
                                 if edges' = [] then
                                   (defnames, Symtab.delete noderef all_edges)
                                 else
-                                  (Symtab.update ((backdefname, ()), defnames),
-                                   Symtab.update ((noderef, edges'), all_edges))
+                                  (Symtab.curried_update (backdefname, ()) defnames,
+                                   Symtab.curried_update (noderef, edges') all_edges)
                               end
                         val defnode' = Defnode (def_ty, all_edges')
-                        val backdefs' = Symtab.update ((backdefname, defnode'), backdefs)
+                        val backdefs' = Symtab.curried_update (backdefname, defnode') backdefs
                         val backclosed' = if backclosed = Closed andalso
                                              Symtab.is_empty all_edges'
                                              andalso no_forwards backdefs'
@@ -557,20 +554,20 @@
                         val backnode' =
                             Node (backty, backdefs', backbacks, backfinals, backclosed')
                       in
-                        (Symtab.update ((backrefname, backnode'), graph), defnames')
+                        (Symtab.curried_update (backrefname, backnode') graph, defnames')
                       end
 
                   val (graph', defnames') =
                       Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
                 in
                   (graph', if Symtab.is_empty defnames' then backs
-                           else Symtab.update ((backrefname, defnames'), backs))
+                           else Symtab.curried_update (backrefname, defnames') backs)
                 end
             val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
             val Node ( _, defs, _, _, closed) = getnode graph' noderef
             val closed = if closed = Closed andalso no_forwards defs then Final else closed
-            val graph' = Symtab.update ((noderef, Node (nodety, defs, backs',
-                                                        finals, closed)), graph')
+            val graph' = Symtab.curried_update (noderef, Node (nodety, defs, backs',
+                                                        finals, closed)) graph'
             val history' = (Finalize (noderef, ty)) :: history
           in
             (cost+1, axmap, history', graph')
@@ -580,14 +577,14 @@
 fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
 
 fun update_axname ax orig_ax (cost, axmap, history, graph) =
-  (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
+  (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph)
 
 fun merge' (Declare cty, g) = declare' g cty
   | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
-    (case Symtab.lookup (graph, name) of
+    (case Symtab.curried_lookup graph name of
        NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
      | SOME (Node (_, defs, _, _, _)) =>
-       (case Symtab.lookup (defs, axname) of
+       (case Symtab.curried_lookup defs axname of
           NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
         | SOME _ => g))
   | merge' (Finalize finals, g) = finalize' g finals
@@ -601,14 +598,14 @@
 fun finals (_, _, history, graph) =
     Symtab.foldl
       (fn (finals, (name, Node(_, _, _, ftys, _))) =>
-          Symtab.update_new ((name, ftys), finals))
+          Symtab.curried_update_new (name, ftys) finals)
       (Symtab.empty, graph)
 
 fun overloading_info (_, axmap, _, graph) c =
     let
-      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
+      fun translate (ax, Defnode (ty, _)) = (the (Symtab.curried_lookup axmap ax), ty)
     in
-      case Symtab.lookup (graph, c) of
+      case Symtab.curried_lookup graph c of
         NONE => NONE
       | SOME (Node (ty, defnodes, _, _, state)) =>
         SOME (ty, map translate (Symtab.dest defnodes), state)
@@ -621,7 +618,7 @@
   | monomorphicT _ = false
 
 fun monomorphic (_, _, _, graph) c =
-  (case Symtab.lookup (graph, c) of
+  (case Symtab.curried_lookup graph c of
     NONE => true
   | SOME (Node (ty, defnodes, _, _, _)) =>
       Symtab.min_key defnodes = Symtab.max_key defnodes andalso

--- a/src/ZF/Tools/induct_tacs.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -70,7 +70,7 @@
 struct
 
 fun datatype_info thy name =
-  (case Symtab.lookup (DatatypesData.get thy, name) of
+  (case Symtab.curried_lookup (DatatypesData.get thy) name of
     SOME info => info
   | NONE => error ("Unknown datatype " ^ quote name));
 
@@ -163,14 +163,12 @@
     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
 
   in
-      thy |> Theory.add_path (Sign.base_name big_rec_name)
-          |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
-          |> DatatypesData.put
-              (Symtab.update
-               ((big_rec_name, dt_info), DatatypesData.get thy))
-          |> ConstructorsData.put
-               (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
-          |> Theory.parent_path
+    thy
+    |> Theory.add_path (Sign.base_name big_rec_name)
+    |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
+    |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy))
+    |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy))
+    |> Theory.parent_path
   end;
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =