src/HOL/Tools/inductive.ML
changeset 42364 8c674b3b8e44
parent 42361 23f352990944
child 42381 309ec68442c6
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -621,8 +621,7 @@
     1.4                let
     1.5                  val k = length Ts;
     1.6                  val bs = map Bound (k - 1 downto 0);
     1.7 -                val P = list_comb (List.nth (preds, i),
     1.8 -                  map (incr_boundvars k) ys @ bs);
     1.9 +                val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
    1.10                  val Q = list_abs (mk_names "x" k ~~ Ts,
    1.11                    HOLogic.mk_binop inductive_conj_name
    1.12                      (list_comb (incr_boundvars k s, bs), P))
    1.13 @@ -641,10 +640,11 @@
    1.14          val SOME (_, i, ys, _) = dest_predicate cs params
    1.15            (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
    1.16  
    1.17 -      in list_all_free (Logic.strip_params r,
    1.18 -        Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    1.19 -          (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
    1.20 -            HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
    1.21 +      in
    1.22 +        list_all_free (Logic.strip_params r,
    1.23 +          Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    1.24 +            (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
    1.25 +              HOLogic.mk_Trueprop (list_comb (nth preds i, ys))))
    1.26        end;
    1.27  
    1.28      val ind_prems = map mk_ind_prem intr_ts;