curried_lookup/update;

--- a/src/Provers/Arith/combine_numerals.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -57,9 +57,9 @@
   | find_repeated (tab, past, t::terms) =
       case try Data.dest_coeff t of
 	  SOME(n,u) => 
-	      (case Termtab.lookup (tab, u) of
+	      (case Termtab.curried_lookup tab u of
 		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
-		| NONE => find_repeated (Termtab.update ((u,n), tab), 
+		| NONE => find_repeated (Termtab.curried_update (u, n) tab, 
 					 t::past,  terms))
 	| NONE => find_repeated (tab, t::past, terms);
 

--- a/src/Pure/Proof/reconstruct.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -81,10 +81,10 @@
             end)
       else (t, T, vTs, env)
   | infer_type sg env Ts vTs (t as Free (s, T)) =
-      if T = dummyT then (case Symtab.lookup (vTs, s) of
+      if T = dummyT then (case Symtab.curried_lookup vTs s of
           NONE =>
             let val (env', T) = mk_tvar (env, [])
-            in (Free (s, T), T, Symtab.update_new ((s, T), vTs), env') end
+            in (Free (s, T), T, Symtab.curried_update_new (s, T) vTs, env') end
         | SOME T => (Free (s, T), T, vTs, env))
       else (t, T, vTs, env)
   | infer_type sg env Ts vTs (Var _) = error "reconstruct_proof: internal error"

--- a/src/Pure/Thy/thm_deps.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -55,10 +55,10 @@
                  | _ => ["global"]);
             in
               if name mem parents' then (gra', parents union parents')
-              else (Symtab.update ((name,
+              else (Symtab.curried_update (name,
                 {name = Sign.base_name name, ID = name,
                  dir = space_implode "/" (session @ prefx),
-                 unfold = false, path = "", parents = parents'}), gra'),
+                 unfold = false, path = "", parents = parents'}) gra',
                name ins parents)
             end
           else (gra, name ins parents)

--- a/src/Pure/envir.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Pure/envir.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -73,7 +73,7 @@
   [T', T], []);
 
 fun gen_lookup f asol (xname, T) =
-  (case Vartab.lookup (asol, xname) of
+  (case Vartab.curried_lookup asol xname of
      NONE => NONE
    | SOME (U, t) => if f (T, U) then SOME t
        else var_clash xname T U);
@@ -92,7 +92,7 @@
 fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
 
 fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
-  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname, (T, t)), asol), iTs=iTs};
+  Envir{maxidx=maxidx, asol=Vartab.curried_update_new (xname, (T, t)) asol, iTs=iTs};
 
 (*The empty environment.  New variables will start with the given index+1.*)
 fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};

--- a/src/Pure/goals.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Pure/goals.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -213,13 +213,13 @@
 
 (* access locales *)
 
-fun get_locale thy name = Symtab.lookup (#locales (LocalesData.get thy), name);
+val get_locale = Symtab.curried_lookup o #locales o LocalesData.get;
 
 fun put_locale (name, locale) thy =
   let
     val {space, locales, scope} = LocalesData.get thy;
     val space' = Sign.declare_name thy name space;
-    val locales' = Symtab.update ((name, locale), locales);
+    val locales' = Symtab.curried_update (name, locale) locales;
   in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
 
 fun lookup_locale thy xname =

--- a/src/ZF/Datatype.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/ZF/Datatype.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -73,9 +73,9 @@
        and (rhead, rargs) = strip_comb rhs
        val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
        val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
-       val lcon_info = valOf (Symtab.lookup (ConstructorsData.get sg, lname))
+       val lcon_info = the (Symtab.curried_lookup (ConstructorsData.get sg) lname)
          handle Option => raise Match;
-       val rcon_info = valOf (Symtab.lookup (ConstructorsData.get sg, rname))
+       val rcon_info = the (Symtab.curried_lookup (ConstructorsData.get sg) rname)
          handle Option => raise Match;
        val new = 
            if #big_rec_name lcon_info = #big_rec_name rcon_info 

--- a/src/ZF/Tools/ind_cases.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -31,7 +31,7 @@
 end);
 
 
-fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab));
+fun declare name f = IndCasesData.map (Symtab.curried_update (name, f));
 
 fun smart_cases thy ss read_prop s =
   let
@@ -40,7 +40,7 @@
     val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
       (Logic.strip_imp_concl A)))))) handle TERM _ => err ();
   in
-    (case Symtab.lookup (IndCasesData.get thy, c) of
+    (case Symtab.curried_lookup (IndCasesData.get thy) c of
       NONE => error ("Unknown inductive cases rule for set " ^ quote c)
     | SOME f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
   end;

--- a/src/ZF/Tools/primrec_package.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -56,7 +56,7 @@
       else strip_comb (hd middle);
     val (cname, _) = dest_Const constr
       handle TERM _ => raise RecError "ill-formed constructor";
-    val con_info = valOf (Symtab.lookup (ConstructorsData.get thy, cname))
+    val con_info = the (Symtab.curried_lookup (ConstructorsData.get thy) cname)
       handle Option =>
       raise RecError "cannot determine datatype associated with function"