--- a/src/HOL/Tools/inductive_realizer.ML Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Oct 29 23:49:55 2009 +0100
@@ -263,8 +263,7 @@
val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
val rlz'' = fold_rev Logic.all vs2 rlz
in (name, (vs,
- if rt = Extraction.nullt then rt else
- List.foldr (uncurry lambda) rt vs1,
+ if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
ProofRewriteRules.un_hhf_proof rlz' rlz''
(fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
end;