src/HOL/Tools/inductive_set.ML
changeset 60781 2da59cdf531c
parent 60642 48dd1cefb4ae
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -223,12 +223,11 @@
     1.4            let
     1.5              val U = HOLogic.dest_setT (body_type T);
     1.6              val Ts = HOLogic.strip_ptupleT fs' U;
     1.7 -            (* FIXME: should cterm_instantiate increment indexes? *)
     1.8              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
     1.9 -            val (arg_cong_f, _) = arg_cong' |> Thm.cprop_of |> Drule.strip_imp_concl |>
    1.10 -              Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb
    1.11 +            val (Var (arg_cong_f, _), _) = arg_cong' |> Thm.concl_of |>
    1.12 +              dest_comb |> snd |> strip_comb |> snd |> hd |> dest_comb;
    1.13            in
    1.14 -            thm' RS (Drule.cterm_instantiate [(arg_cong_f,
    1.15 +            thm' RS (infer_instantiate ctxt [(arg_cong_f,
    1.16                Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
    1.17                  HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
    1.18                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)