# HG changeset patch
# User wenzelm
# Date 1139255996 -3600
# Node ID c050ae1f8f52545867f67125ff1d780b9a6a3e8f
# Parent  fa71f2ddd2e8e988e20d39bcbac77093c3298d16
Envir.(beta_)eta_contract;
TableFun: renamed xxx_multi to xxx_list;

diff -r fa71f2ddd2e8 -r c050ae1f8f52 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Feb 06 20:59:55 2006 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Feb 06 20:59:56 2006 +0100
@@ -80,7 +80,7 @@
 
 fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
   {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
-     (Pattern.eta_contract lhs, (next, r)) net};
+     (Envir.eta_contract lhs, (next, r)) net};
 
 fun merge_rules
   ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
@@ -113,7 +113,7 @@
         in SOME (Envir.norm_term env'' (inc (ren tm2)))
         end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
           (sort (int_ord o pairself fst)
-            (Net.match_term rules (Pattern.eta_contract tm)))
+            (Net.match_term rules (Envir.eta_contract tm)))
       end;
 
   in rew end;
@@ -205,8 +205,7 @@
     {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
      typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
      types = merge_alists types1 types2,
-     realizers = Symtab.merge_multi' (eq_set o pairself #1)
-       (realizers1, realizers2),
+     realizers = Symtab.merge_list (eq_set o pairself #1) (realizers1, realizers2),
      defs = gen_merge_lists eq_thm defs1 defs2,
      expand = merge_lists expand1 expand2,
      prep = (case prep1 of NONE => prep2 | _ => prep1)};
@@ -300,7 +299,7 @@
   in
     ExtractionData.put
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
-       realizers = fold (Symtab.update_multi o prep_rlz thy) rs realizers,
+       realizers = fold (Symtab.update_list o prep_rlz thy) rs realizers,
        defs = defs, expand = expand, prep = prep} thy
   end
 
@@ -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.lookup_list 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
@@ -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.lookup_list 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