src/HOL/Tools/inductive_set_package.ML
changeset 26806 40b411ec05aa
parent 26534 a2cb4de2a1aa
child 26988 742e26213212
     1.1 --- a/src/HOL/Tools/inductive_set_package.ML	Wed May 07 10:56:58 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Wed May 07 10:57:19 2008 +0200
     1.3 @@ -237,7 +237,7 @@
     1.4          NONE => thm' RS sym
     1.5        | SOME fs' =>
     1.6            let
     1.7 -            val U = HOLogic.dest_setT (body_type T);
     1.8 +            val (_, U) = split_last (binder_types T);
     1.9              val Ts = HOLogic.prodT_factors' fs' U;
    1.10              (* FIXME: should cterm_instantiate increment indexes? *)
    1.11              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
    1.12 @@ -413,7 +413,7 @@
    1.13        | infer (t $ u) = infer t #> infer u
    1.14        | infer _ = I;
    1.15      val new_arities = filter_out
    1.16 -      (fn (x as Free (_, Type ("fun", _)), _) => x mem params
    1.17 +      (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
    1.18          | _ => false) (fold (snd #> infer) intros []);
    1.19      val params' = map (fn x => (case AList.lookup op = new_arities x of
    1.20          SOME fs =>
    1.21 @@ -437,7 +437,7 @@
    1.22      val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
    1.23        let
    1.24          val fs = the_default [] (AList.lookup op = new_arities c);
    1.25 -        val U = HOLogic.dest_setT (body_type T);
    1.26 +        val (_, U) = split_last (binder_types T);
    1.27          val Ts = HOLogic.prodT_factors' fs U;
    1.28          val c' = Free (s ^ "p",
    1.29            map fastype_of params1 @ Ts ---> HOLogic.boolT)