Envir.(beta_)eta_contract;
authorwenzelm
Mon Feb 06 20:59:56 2006 +0100 (2006-02-06)
changeset 18956c050ae1f8f52
parent 18955 fa71f2ddd2e8
child 18957 8c3abd63bce3
Envir.(beta_)eta_contract;
TableFun: renamed xxx_multi to xxx_list;
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Feb 06 20:59:55 2006 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Feb 06 20:59:56 2006 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  
     1.5  fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
     1.6    {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
     1.7 -     (Pattern.eta_contract lhs, (next, r)) net};
     1.8 +     (Envir.eta_contract lhs, (next, r)) net};
     1.9  
    1.10  fun merge_rules
    1.11    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    1.12 @@ -113,7 +113,7 @@
    1.13          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    1.14          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
    1.15            (sort (int_ord o pairself fst)
    1.16 -            (Net.match_term rules (Pattern.eta_contract tm)))
    1.17 +            (Net.match_term rules (Envir.eta_contract tm)))
    1.18        end;
    1.19  
    1.20    in rew end;
    1.21 @@ -205,8 +205,7 @@
    1.22      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
    1.23       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    1.24       types = merge_alists types1 types2,
    1.25 -     realizers = Symtab.merge_multi' (eq_set o pairself #1)
    1.26 -       (realizers1, realizers2),
    1.27 +     realizers = Symtab.merge_list (eq_set o pairself #1) (realizers1, realizers2),
    1.28       defs = gen_merge_lists eq_thm defs1 defs2,
    1.29       expand = merge_lists expand1 expand2,
    1.30       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.31 @@ -300,7 +299,7 @@
    1.32    in
    1.33      ExtractionData.put
    1.34        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
    1.35 -       realizers = fold (Symtab.update_multi o prep_rlz thy) rs realizers,
    1.36 +       realizers = fold (Symtab.update_list o prep_rlz thy) rs realizers,
    1.37         defs = defs, expand = expand, prep = prep} thy
    1.38    end
    1.39  
    1.40 @@ -601,7 +600,7 @@
    1.41            in
    1.42              if etype_of thy' vs' [] prop = nullT andalso
    1.43                realizes_null vs' prop aconv prop then (defs, prf0)
    1.44 -            else case find vs' (Symtab.lookup_multi realizers s) of
    1.45 +            else case find vs' (Symtab.lookup_list realizers s) of
    1.46                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
    1.47              | NONE => error ("corr: no realizer for instance of axiom " ^
    1.48                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    1.49 @@ -708,7 +707,7 @@
    1.50              val (vs', tye) = find_inst prop Ts ts vs;
    1.51              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.52            in
    1.53 -            case find vs' (Symtab.lookup_multi realizers s) of
    1.54 +            case find vs' (Symtab.lookup_list realizers s) of
    1.55                SOME (t, _) => (defs, subst_TVars tye' t)
    1.56              | NONE => error ("extr: no realizer for instance of axiom " ^
    1.57                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm