src/HOL/Tools/inductive_package.ML
changeset 30190 479806475f3c
parent 30089 f631fb528277
child 30218 cdd82ba2b4fd
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -517,7 +517,7 @@
     1.4            (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
     1.5  
     1.6        in list_all_free (Logic.strip_params r,
     1.7 -        Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
     1.8 +        Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem
     1.9            [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
    1.10              HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
    1.11        end;
    1.12 @@ -541,7 +541,7 @@
    1.13      (* make predicate for instantiation of abstract induction rule *)
    1.14  
    1.15      val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
    1.16 -      (map_index (fn (i, P) => foldr HOLogic.mk_imp
    1.17 +      (map_index (fn (i, P) => List.foldr HOLogic.mk_imp
    1.18           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
    1.19           (make_bool_args HOLogic.mk_not I bs i)) preds));
    1.20  
    1.21 @@ -624,7 +624,7 @@
    1.22            map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
    1.23            map (subst o HOLogic.dest_Trueprop)
    1.24              (Logic.strip_assums_hyp r)
    1.25 -      in foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
    1.26 +      in List.foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
    1.27          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
    1.28          (Logic.strip_params r)
    1.29        end