src/Pure/type.ML

     fun cert (T as Type (c, Ts)) =
           let
             val Ts' = map cert Ts;
             fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
           in
-            (case Symtab.curried_lookup types c of
+            (case Symtab.lookup types c of
               SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
             | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
                 if syn then check_syntax c else ();
                 if normalize then inst_typ (vs ~~ Ts') U
                 else Type (c, Ts'))

 fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   [TVar (ixn, S), TVar (ixn, S')], []);
 
 fun lookup (tye, (ixn, S)) =
-  (case Vartab.curried_lookup tye ixn of
+  (case Vartab.lookup tye ixn of
     NONE => NONE
   | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
 
 
 (* matching *)

 fun typ_match tsig =
   let
     fun match (TVar (v, S), T) subs =
           (case lookup (subs, (v, S)) of
             NONE =>
-              if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs
+              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
               else raise TYPE_MATCH
           | SOME U => if U = T then subs else raise TYPE_MATCH)
       | match (Type (a, Ts), Type (b, Us)) subs =
           if a <> b then raise TYPE_MATCH
           else matches (Ts, Us) subs

   (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
 
 (*purely structural matching*)
 fun raw_match (TVar (v, S), T) subs =
       (case lookup (subs, (v, S)) of
-        NONE => Vartab.curried_update_new (v, (S, T)) subs
+        NONE => Vartab.update_new (v, (S, T)) subs
       | SOME U => if U = T then subs else raise TYPE_MATCH)
   | raw_match (Type (a, Ts), Type (b, Us)) subs =
       if a <> b then raise TYPE_MATCH
       else raw_matches (Ts, Us) subs
   | raw_match (TFree x, TFree y) subs =

       Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
 
     fun meet (_, []) tye = tye
       | meet (TVar (xi, S'), S) tye =
           if Sorts.sort_le classes (S', S) then tye
-          else Vartab.curried_update_new
+          else Vartab.update_new
             (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye
       | meet (TFree (_, S'), S) tye =
           if Sorts.sort_le classes (S', S) then tye
           else raise TUNIFY
       | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye

       (case (devar tye ty1, devar tye ty2) of
         (T as TVar (v, S1), U as TVar (w, S2)) =>
           if eq_ix (v, w) then
             if S1 = S2 then tye else tvar_clash v S1 S2
           else if Sorts.sort_le classes (S1, S2) then
-            Vartab.curried_update_new (w, (S2, T)) tye
+            Vartab.update_new (w, (S2, T)) tye
           else if Sorts.sort_le classes (S2, S1) then
-            Vartab.curried_update_new (v, (S1, U)) tye
+            Vartab.update_new (v, (S1, U)) tye
           else
             let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
-              Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye)
+              Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye)
             end
       | (TVar (v, S), T) =>
           if occurs v tye T then raise TUNIFY
-          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
+          else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
       | (T, TVar (v, S)) =>
           if occurs v tye T then raise TUNIFY
-          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
+          else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
       | (Type (a, Ts), Type (b, Us)) =>
           if a <> b then raise TUNIFY
           else unifs (Ts, Us) tye
       | (T, U) => if T = U then tye else raise TUNIFY)
     and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye)

 fun raw_unify (ty1, ty2) tye =
   (case (devar tye ty1, devar tye ty2) of
     (T as TVar (v, S1), U as TVar (w, S2)) =>
       if eq_ix (v, w) then
         if S1 = S2 then tye else tvar_clash v S1 S2
-      else Vartab.curried_update_new (w, (S2, T)) tye
+      else Vartab.update_new (w, (S2, T)) tye
   | (TVar (v, S), T) =>
       if occurs v tye T then raise TUNIFY
-      else Vartab.curried_update_new (v, (S, T)) tye
+      else Vartab.update_new (v, (S, T)) tye
   | (T, TVar (v, S)) =>
       if occurs v tye T then raise TUNIFY
-      else Vartab.curried_update_new (v, (S, T)) tye
+      else Vartab.update_new (v, (S, T)) tye
   | (Type (a, Ts), Type (b, Us)) =>
       if a <> b then raise TUNIFY
       else raw_unifys (Ts, Us) tye
   | (T, U) => if T = U then tye else raise TUNIFY)
 and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)

 
 fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
 
 fun insert_arities pp classes (t, ars) arities =
   let val ars' =
-    Symtab.curried_lookup_multi arities t
+    Symtab.lookup_multi arities t
     |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
-  in Symtab.curried_update (t, ars') arities end;
+  in Symtab.update (t, ars') arities end;
 
 fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
   insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
 
 in
 
 fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   let
     fun prep (t, Ss, S) =
-      (case Symtab.curried_lookup (#2 types) t of
+      (case Symtab.lookup (#2 types) t of
         SOME (LogicalType n, _) =>
           if length Ss = n then
             (t, map (cert_sort tsig) Ss, cert_sort tsig S)
               handle TYPE (msg, _, _) => error msg
           else error (bad_nargs t)

 fun new_decl naming (c, decl) (space, types) =
   let
     val c' = NameSpace.full naming c;
     val space' = NameSpace.declare naming c' space;
     val types' =
-      (case Symtab.curried_lookup types c' of
+      (case Symtab.lookup types c' of
         SOME (decl', _) => err_in_decls c' decl decl'
-      | NONE => Symtab.curried_update (c', (decl, stamp ())) types);
+      | NONE => Symtab.update (c', (decl, stamp ())) types);
   in (space', types') end;
 
-fun the_decl (_, types) = fst o the o Symtab.curried_lookup types;
+fun the_decl (_, types) = fst o the o Symtab.lookup types;
 
 fun change_types f = map_tsig (fn (classes, default, types, arities) =>
   (classes, default, f types, arities));
 
 fun syntactic types (Type (c, Ts)) =
-      (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false)
+      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
         orelse exists (syntactic types) Ts
   | syntactic _ _ = false;
 
 fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   let