src/Pure/Proof/extraction.ML
changeset 17223 430edc6b7826
parent 17203 29b2563f5c11
child 17232 148c241d2492
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Sep 01 18:48:54 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Sep 01 22:15:10 2005 +0200
     1.3 @@ -301,8 +301,7 @@
     1.4    in
     1.5      ExtractionData.put
     1.6        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
     1.7 -       realizers = foldr Symtab.update_multi
     1.8 -         realizers (map (prep_rlz thy) (rev rs)),
     1.9 +       realizers = fold (Symtab.curried_update_multi o prep_rlz thy) rs realizers,
    1.10         defs = defs, expand = expand, prep = prep} thy
    1.11    end
    1.12  
    1.13 @@ -565,7 +564,7 @@
    1.14                else fst (extr d defs vs ts Ts hs prf0)
    1.15            in
    1.16              if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
    1.17 -            else case Symtab.lookup (realizers, name) of
    1.18 +            else case Symtab.curried_lookup realizers name of
    1.19                NONE => (case find vs' (find' name defs') of
    1.20                  NONE =>
    1.21                    let
    1.22 @@ -601,7 +600,7 @@
    1.23            in
    1.24              if etype_of thy' vs' [] prop = nullT andalso
    1.25                realizes_null vs' prop aconv prop then (defs, prf0)
    1.26 -            else case find vs' (Symtab.lookup_multi (realizers, s)) of
    1.27 +            else case find vs' (Symtab.curried_lookup_multi realizers s) of
    1.28                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
    1.29              | NONE => error ("corr: no realizer for instance of axiom " ^
    1.30                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    1.31 @@ -649,7 +648,7 @@
    1.32              val (vs', tye) = find_inst prop Ts ts vs;
    1.33              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.34            in
    1.35 -            case Symtab.lookup (realizers, s) of
    1.36 +            case Symtab.curried_lookup realizers s of
    1.37                NONE => (case find vs' (find' s defs) of
    1.38                  NONE =>
    1.39                    let
    1.40 @@ -708,7 +707,7 @@
    1.41              val (vs', tye) = find_inst prop Ts ts vs;
    1.42              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.43            in
    1.44 -            case find vs' (Symtab.lookup_multi (realizers, s)) of
    1.45 +            case find vs' (Symtab.curried_lookup_multi realizers s) of
    1.46                SOME (t, _) => (defs, subst_TVars tye' t)
    1.47              | NONE => error ("extr: no realizer for instance of axiom " ^
    1.48                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm