# HG changeset patch
# User berghofe
# Date 1238746146 -7200
# Node ID 294e8ee163ea37c0e0bacca81a80b5b369aaf6d2
# Parent  29eb80cef6b74f0f683c1876361312a554f30ec7# Parent  e5f9477aed50953d1009b01016bf2abb76066dfa
merged

diff -r 29eb80cef6b7 -r 294e8ee163ea src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Fri Apr 03 09:27:31 2009 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Fri Apr 03 10:09:06 2009 +0200
@@ -435,12 +435,19 @@
        | NONE => (x, (x, (x, x))))) params;
     val (params1, (params2, params3)) =
       params' |> map snd |> split_list ||> split_list;
+    val paramTs = map fastype_of params;
 
     (* 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) = split_last (binder_types T);
+        val (Us, U) = split_last (binder_types T);
+        val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks
+          [Pretty.str "Argument types",
+           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) Us)),
+           Pretty.str ("of " ^ s ^ " do not agree with types"),
+           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
+           Pretty.str "of declared parameters"]));
         val Ts = HOLogic.prodT_factors' fs U;
         val c' = Free (s ^ "p",
           map fastype_of params1 @ Ts ---> HOLogic.boolT)