src/Pure/Proof/extraction.ML

   let val {realizes_eqns, typeof_eqns, types, realizers,
     defs, expand, prep} = ExtractionData.get thy
   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
 
 fun prep_realizer thy =
   let

             val T = etype_of thy' vs' [] prop;
             val defs' = if T = nullT then defs
               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
                     val _ = assert (T = nullT) "corr: internal error";
                     val _ = msg d ("Building correctness proof for " ^ quote name ^

             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
           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
                   (Reconstruct.prop_of (proof_combt (prf0, ts)))))
           end

       | extr d defs vs ts Ts hs (prf0 as PThm ((s, _), prf, prop, SOME Ts')) =
           let
             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
                     val _ = msg d ("Extracting " ^ quote s ^
                       (if null vs' then ""

       | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
           let
             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
                   (Reconstruct.prop_of (proof_combt (prf0, ts)))))
           end