src/HOL/Tools/inductive_set_package.ML

     val thm' = Thm.instantiate ([], insts) thm;
     val thm'' = (case optfs' of
         NONE => thm' RS sym
       | SOME fs' =>
           let
-            val U = HOLogic.dest_setT (body_type T);
+            val (_, U) = split_last (binder_types T);
             val Ts = HOLogic.prodT_factors' fs' U;
             (* FIXME: should cterm_instantiate increment indexes? *)
             val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
             val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
               Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb

       | infer (Const ("op :", _) $ t $ u) =
           infer_arities thy set_arities (SOME (HOLogic.prod_factors t), u)
       | infer (t $ u) = infer t #> infer u
       | infer _ = I;
     val new_arities = filter_out
-      (fn (x as Free (_, Type ("fun", _)), _) => x mem params
+      (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
         | _ => false) (fold (snd #> infer) intros []);
     val params' = map (fn x => (case AList.lookup op = new_arities x of
         SOME fs =>
           let
             val T = HOLogic.dest_setT (fastype_of x);

 
     (* equations for converting sets to predicates *)
     val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
       let
         val fs = the_default [] (AList.lookup op = new_arities c);
-        val U = HOLogic.dest_setT (body_type T);
+        val (_, U) = split_last (binder_types T);
         val Ts = HOLogic.prodT_factors' fs U;
         val c' = Free (s ^ "p",
           map fastype_of params1 @ Ts ---> HOLogic.boolT)
       in
         ((c', (fs, U, Ts)),