src/Pure/Isar/locale.ML

 (* instantiate TFrees *)
 
 fun tinst_tab_type tinst T = if Symtab.is_empty tinst
       then T
       else Term.map_type_tfree
-        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
+        (fn (v as (x, _)) => getOpt (Symtab.curried_lookup tinst x, (TFree v))) T;
 
 fun tinst_tab_term tinst t = if Symtab.is_empty tinst
       then t
       else Term.map_term_types (tinst_tab_type tinst) t;
 

 fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
       then tinst_tab_term tinst
       else (* instantiate terms and types simultaneously *)
         let
           fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
-            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
+            | instf (Free (x, T)) = (case Symtab.curried_lookup inst x of
                  NONE => Free (x, tinst_tab_type tinst T)
                | SOME t => t)
             | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
             | instf (b as Bound _) = b
             | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t)

     in (case subs of
         [] => let
                 val sups =
                   List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
                 val sups' = map (apfst untermify) sups
-              in (Termtab.update ((t, (attn, [])), regs), sups') end
+              in (Termtab.curried_update (t, (attn, [])) regs, sups') end
       | _ => (regs, []))
     end;
 
   (* add witness theorem to registration,
      only if instantiation is exact, otherwise exception Option raised *)
   fun add_witness ts thm regs =
     let
       val t = termify ts;
-      val (x, thms) = valOf (Termtab.lookup (regs, t));
+      val (x, thms) = valOf (Termtab.curried_lookup regs t);
     in
-      Termtab.update ((t, (x, thm::thms)), regs)
+      Termtab.curried_update (t, (x, thm::thms)) regs
     end;
 end;
 
 
 (** theory data **)

   thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
     (Sign.declare_name thy name space, locs, regs));
 
 fun put_locale name loc =
   GlobalLocalesData.map (fn (space, locs, regs) =>
-    (space, Symtab.update ((name, loc), locs), regs));
-
-fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name);
+    (space, Symtab.curried_update (name, loc) locs, regs));
+
+fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name;
 
 fun the_locale thy name =
   (case get_locale thy name of
     SOME loc => loc
   | NONE => error ("Unknown locale " ^ quote name));

    Thms of registrations are never varified. *)
 
 (* retrieve registration from theory or context *)
 
 fun gen_get_registrations get thy_ctxt name =
-  case Symtab.lookup (get thy_ctxt, name) of
+  case Symtab.curried_lookup (get thy_ctxt) name of
       NONE => []
     | SOME reg => Registrations.dest reg;
 
 val get_global_registrations =
      gen_get_registrations (#3 o GlobalLocalesData.get);
 val get_local_registrations =
      gen_get_registrations LocalLocalesData.get;
 
 fun gen_get_registration get thy_of thy_ctxt (name, ps) =
-  case Symtab.lookup (get thy_ctxt, name) of
+  case Symtab.curried_lookup (get thy_ctxt) name of
       NONE => NONE
     | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
 
 val get_global_registration =
      gen_get_registration (#3 o GlobalLocalesData.get) I;

 
 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
   map_data (fn regs =>
     let
       val thy = thy_of thy_ctxt;
-      val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
+      val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty);
       val (reg', sups) = Registrations.insert thy (ps, attn) reg;
       val _ = if not (null sups) then warning
                 ("Subsumed interpretation(s) of locale " ^
                  quote (extern thy name) ^
                  "\nby interpretation(s) with the following prefix(es):\n" ^
                   commas_quote (map (fn (_, ((s, _), _)) => s) sups))
               else ();
-    in Symtab.update ((name, reg'), regs) end) thy_ctxt;
+    in Symtab.curried_update (name, reg') regs end) thy_ctxt;
 
 val put_global_registration =
      gen_put_registration (fn f =>
        GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
 val put_local_registration =

 
 
 (* add witness theorem to registration in theory or context,
    ignored if registration not present *)
 
-fun gen_add_witness map (name, ps) thm =
-  map (fn regs =>
-      let
-        val reg = valOf (Symtab.lookup (regs, name));
-      in
-        Symtab.update ((name, Registrations.add_witness ps thm reg), regs)
-      end handle Option => regs);
+fun gen_add_witness map_regs (name, ps) thm =
+  map_regs (Symtab.map_entry name (Registrations.add_witness ps thm));
 
 val add_global_witness =
      gen_add_witness (fn f =>
        GlobalLocalesData.map (fn (space, locs, regs) =>
          (space, locs, f regs)));

           else Pretty.block ((prt_attn attn @
             [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
 
     val loc_int = intern thy loc;
     val regs = get_regs thy_ctxt;
-    val loc_regs = Symtab.lookup (regs, loc_int);
+    val loc_regs = Symtab.curried_lookup regs loc_int;
   in
     (case loc_regs of
         NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
       | SOME r => let
             val r' = Registrations.dest r;

 
 fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
 fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
 fun params_syn_of syn elemss =
   gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
-    map (apfst (fn x => (x, valOf (Symtab.lookup (syn, x)))));
+    map (apfst (fn x => (x, valOf (Symtab.curried_lookup syn x))));
 
 
 (* CB: param_types has the following type:
   ('a * 'b option) list -> ('a * 'b) list *)
 fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;

     fun eval syn ((name, xs), axs) =
       let
         val {params = (ps, qs), elems, ...} = the_locale thy name;
         val ps' = map (apsnd SOME o #1) ps;
         val ren = map #1 ps' ~~
-              map (fn x => (x, valOf (Symtab.lookup (syn, x)))) xs;
+              map (fn x => (x, valOf (Symtab.curried_lookup syn x))) xs;
         val (params', elems') =
           if null ren then ((ps', qs), map #1 elems)
           else ((map (apfst (rename ren)) ps', map (rename ren) qs),
             map (rename_elem ren o #1) elems);
         val elems'' = map (rename_facts (space_implode "_" xs)) elems';

     val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
     val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
         |> Symtab.make;            
     (* replace parameter names in ids by instantiations *)
     val vinst = Symtab.make (parms ~~ vts);
-    fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
+    fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps;
     val inst = Symtab.make (parms ~~ ts);
     val ids' = map (apsnd vinst_names) ids;
     val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
   in ((inst, tinst), wits) end;
 

     |> note_thmss_qualified "" name facts' |> #1
     |> declare_locale name
     |> put_locale name {predicate = predicate, import = import,
         elems = map (fn e => (e, stamp ())) elems',
         params = (params_of elemss' |>
-          map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)),
+          map (fn (x, SOME T) => ((x, T), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)),
         regs = []}
     |> pair (elems', body_ctxt)
   end;
 
 in

       let
         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
                NONE => error ("Instance missing for parameter " ^ quote p)
              | SOME (Free (_, T), t) => (t, T);
         val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
-      in (Symtab.update_new ((p, d), inst), tinst) end;
+      in (Symtab.curried_update_new (p, d) inst, tinst) end;
     val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
     (* Note: inst and tinst contain no vars. *)
 
     (** compute proof obligations **)