# HG changeset patch
# User berghofe
# Date 1331133229 -3600
# Node ID b1d15637381aedea9aaca58a40756735240b3b7f
# Parent  9f82058567ce185eba62b97136c4e8b0cfc88570
to_pred/set attributes now properly handle variables of type "... => T set"

diff -r 9f82058567ce -r b1d15637381a src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Mar 07 14:30:35 2012 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Wed Mar 07 16:13:49 2012 +0100
@@ -227,12 +227,16 @@
 fun mk_to_pred_inst thy fs =
   map (fn (x, ps) =>
     let
-      val U = HOLogic.dest_setT (fastype_of x);
-      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
+      val (Ts, T) = strip_type (fastype_of x);
+      val U = HOLogic.dest_setT T;
+      val x' = map_type
+        (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
     in
       (cterm_of thy x,
-       cterm_of thy (HOLogic.Collect_const U $
-         HOLogic.mk_psplits ps U HOLogic.boolT x'))
+       cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+         (HOLogic.Collect_const U $
+            HOLogic.mk_psplits ps U HOLogic.boolT
+              (list_comb (x', map Bound (length Ts - 1 downto 0))))))
     end) fs;
 
 fun mk_to_pred_eq p fs optfs' T thm =
@@ -366,12 +370,16 @@
     val insts = map (fn (x, ps) =>
       let
         val Ts = binder_types (fastype_of x);
-        val T = HOLogic.mk_ptupleT ps Ts;
-        val x' = map_type (K (HOLogic.mk_setT T)) x
+        val l = length Ts;
+        val k = length ps;
+        val (Rs, Us) = chop (l - k - 1) Ts;
+        val T = HOLogic.mk_ptupleT ps Us;
+        val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
       in
         (cterm_of thy x,
          cterm_of thy (fold_rev (Term.abs o pair "x") Ts
-          (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
+          (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
+             list_comb (x', map Bound (l - 1 downto k + 1))))))
       end) fs;
   in
     thm |>