diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -205,7 +205,7 @@
       val x' = map_type
         (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
     in
-      (Thm.cterm_of ctxt x,
+      (dest_Var x,
        Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
          (HOLogic.Collect_const U $
             HOLogic.mk_psplits ps U HOLogic.boolT
@@ -367,7 +367,7 @@
         val T = HOLogic.mk_ptupleT ps Us;
         val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
       in
-        (Thm.cterm_of ctxt x,
+        (dest_Var x,
          Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
           (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
              list_comb (x', map Bound (l - 1 downto k + 1))))))