src/HOL/Tools/inductive_realizer.ML
changeset 33338 de76079f973a
parent 33244 db230399f890
child 33666 e49bfeb0d822
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:48:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:49:55 2009 +0100
     1.3 @@ -263,8 +263,7 @@
     1.4      val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
     1.5      val rlz'' = fold_rev Logic.all vs2 rlz
     1.6    in (name, (vs,
     1.7 -    if rt = Extraction.nullt then rt else
     1.8 -      List.foldr (uncurry lambda) rt vs1,
     1.9 +    if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    1.10      ProofRewriteRules.un_hhf_proof rlz' rlz''
    1.11        (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
    1.12    end;