--- a/src/Pure/Proof/extraction.ML Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Sep 01 22:15:10 2005 +0200
@@ -301,8 +301,7 @@
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
@@ -565,7 +564,7 @@
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
@@ -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.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
@@ -649,7 +648,7 @@
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
@@ -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.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