src/Pure/proofterm.ML
changeset 23178 07ba6b58b3d2
parent 22846 fb79144af9a3
child 23296 25f28f9c28a3
     1.1 --- a/src/Pure/proofterm.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -250,7 +250,7 @@
     1.4        (PThm (_, prf', _, _), _) => prf'
     1.5      | _ => prf);
     1.6  
     1.7 -val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
     1.8 +val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
     1.9  fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
    1.10  
    1.11  fun apsome f NONE = raise SAME
    1.12 @@ -621,7 +621,7 @@
    1.13    let
    1.14      val used = it_term_types add_typ_tfree_names (t, [])
    1.15      and tvars = map #1 (it_term_types add_typ_tvars (t, []));
    1.16 -    val (alist, _) = foldr new_name ([], used) tvars;
    1.17 +    val (alist, _) = List.foldr new_name ([], used) tvars;
    1.18    in
    1.19      (case alist of
    1.20        [] => prf (*nothing to do!*)
    1.21 @@ -643,9 +643,9 @@
    1.22      val j = length Bs;
    1.23    in
    1.24      mk_AbsP (j+1, proof_combP (prf, map PBound
    1.25 -      (j downto 1) @ [mk_Abst (mk_AbsP (i,
    1.26 +      (j downto 1) @ [mk_Abst params (mk_AbsP (i,
    1.27          proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
    1.28 -          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m)))))) params]))
    1.29 +          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
    1.30    end;
    1.31  
    1.32  
    1.33 @@ -700,7 +700,7 @@
    1.34      val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
    1.35      val k = length ps;
    1.36  
    1.37 -    fun mk_app (b, (i, j, prf)) =
    1.38 +    fun mk_app b (i, j, prf) =
    1.39            if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
    1.40  
    1.41      fun lift Us bs i j (Const ("==>", _) $ A $ B) =
    1.42 @@ -708,7 +708,7 @@
    1.43        | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
    1.44              Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
    1.45        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
    1.46 -            map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
    1.47 +            map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
    1.48                (i + k - 1 downto i));
    1.49    in
    1.50      mk_AbsP (k, lift [] [] 0 0 Bi)
    1.51 @@ -1200,7 +1200,7 @@
    1.52        map SOME (sort Term.term_ord (term_frees prop));
    1.53      val opt_prf = if ! proofs = 2 then
    1.54          #4 (shrink_proof thy [] 0 (rewrite_prf fst (ProofData.get thy)
    1.55 -          (foldr (uncurry implies_intr_proof) prf hyps)))
    1.56 +          (fold_rev implies_intr_proof hyps prf)))
    1.57        else MinProof (mk_min_proof prf ([], [], []));
    1.58      val head = (case strip_combt (fst (strip_combP prf)) of
    1.59          (PThm (old_name, prf', prop', NONE), args') =>