1.1 --- a/src/HOL/Tools/inductive_set_package.ML	Fri Apr 03 09:27:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Fri Apr 03 10:09:06 2009 +0200
     1.3 @@ -435,12 +435,19 @@
     1.4         | NONE => (x, (x, (x, x))))) params;
     1.5      val (params1, (params2, params3)) =
     1.6        params' |> map snd |> split_list ||> split_list;
     1.7 +    val paramTs = map fastype_of params;
     1.8  
     1.9      (* equations for converting sets to predicates *)
    1.10      val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
    1.11        let
    1.12          val fs = the_default [] (AList.lookup op = new_arities c);
    1.13 -        val (_, U) = split_last (binder_types T);
    1.14 +        val (Us, U) = split_last (binder_types T);
    1.15 +        val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks
    1.16 +          [Pretty.str "Argument types",
    1.17 +           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) Us)),
    1.18 +           Pretty.str ("of " ^ s ^ " do not agree with types"),
    1.19 +           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
    1.20 +           Pretty.str "of declared parameters"]));
    1.21          val Ts = HOLogic.prodT_factors' fs U;
    1.22          val c' = Free (s ^ "p",
    1.23            map fastype_of params1 @ Ts ---> HOLogic.boolT)