# 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