diff -r 8fc868e9e1bf -r 308ebcd2f5dc src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Fri Sep 08 00:02:22 2017 +0200
@@ -263,13 +263,13 @@
   |> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts))))
   |> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts)));
 
-fun typedef_of ctxt whacks T_name =
+fun typedef_of ctxt T_name =
   if T_name = @{type_name set} then
     let
       val A = Logic.varifyT_global @{typ 'a};
       val absT = Type (@{type_name set}, [A]);
       val repT = A --> HOLogic.boolT;
-      val pred = K (Abs (Name.uu, repT, @{const True}));
+      val pred = Abs (Name.uu, repT, @{const True});
       val abs = Const (@{const_name Collect}, repT --> absT);
       val rep = Const (@{const_name rmember}, absT --> repT);
     in
@@ -284,25 +284,21 @@
       let
         val absT = Logic.varifyT_global abs_type;
         val repT = Logic.varifyT_global rep_type;
-        val set0 = Thm.prop_of Rep
+        val set = Thm.prop_of Rep
           |> HOLogic.dest_Trueprop
           |> HOLogic.dest_mem
           |> snd;
-        val pred0 = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set0));
-        fun pred () = preprocess_prop false ctxt whacks pred0;
+        val pred = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set));
         val abs = Const (Abs_name, repT --> absT);
         val rep = Const (Rep_name, absT --> repT);
       in
         (absT, repT, pred, abs, rep)
       end);
 
-fun quotient_of ctxt whacks T_name =
+fun quotient_of ctxt T_name =
   (case Quotient_Info.lookup_quotients ctxt T_name of
-    SOME {equiv_rel = equiv_rel0, qtyp, rtyp, quot_thm, ...} =>
-    let
-      val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm;
-      fun equiv_rel () = preprocess_prop false ctxt whacks equiv_rel0;
-    in
+    SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} =>
+    let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in
       (qtyp, rtyp, equiv_rel, abs, rep)
     end);
 
@@ -354,64 +350,60 @@
 
 val is_co_datatype_case = can o dest_co_datatype_case;
 
-fun is_quotient_abs ctxt whacks (s, T) =
+fun is_quotient_abs ctxt (s, T) =
   (case T of
     Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
     classify_type_name ctxt absT_name = Quotient andalso
-    (case quotient_of ctxt whacks absT_name of
+    (case quotient_of ctxt absT_name of
       (_, _, _, Const (s', _), _) => s' = s)
   | _ => false);
 
-fun is_quotient_rep ctxt whacks (s, T) =
+fun is_quotient_rep ctxt (s, T) =
   (case T of
     Type (@{type_name fun}, [Type (absT_name, _), _]) =>
     classify_type_name ctxt absT_name = Quotient andalso
-    (case quotient_of ctxt whacks absT_name of
+    (case quotient_of ctxt absT_name of
       (_, _, _, _, Const (s', _)) => s' = s)
   | _ => false);
 
-fun is_maybe_typedef_abs ctxt whacks absT_name s =
+fun is_maybe_typedef_abs ctxt absT_name s =
   if absT_name = @{type_name set} then
     s = @{const_name Collect}
   else
-    (case try (typedef_of ctxt whacks) absT_name of
+    (case try (typedef_of ctxt) absT_name of
       SOME (_, _, _, Const (s', _), _) => s' = s
     | NONE => false);
 
-fun is_maybe_typedef_rep ctxt whacks absT_name s =
+fun is_maybe_typedef_rep ctxt absT_name s =
   if absT_name = @{type_name set} then
     s = @{const_name rmember}
   else
-    (case try (typedef_of ctxt whacks) absT_name of
+    (case try (typedef_of ctxt) absT_name of
       SOME (_, _, _, _, Const (s', _)) => s' = s
     | NONE => false);
 
-fun is_typedef_abs ctxt whacks (s, T) =
+fun is_typedef_abs ctxt (s, T) =
   (case T of
     Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
-    classify_type_name ctxt absT_name = Typedef andalso
-    is_maybe_typedef_abs ctxt whacks absT_name s
+    classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_abs ctxt absT_name s
   | _ => false);
 
-fun is_typedef_rep ctxt whacks (s, T) =
+fun is_typedef_rep ctxt (s, T) =
   (case T of
     Type (@{type_name fun}, [Type (absT_name, _), _]) =>
-    classify_type_name ctxt absT_name = Typedef andalso
-    is_maybe_typedef_rep ctxt whacks absT_name s
+    classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_rep ctxt absT_name s
   | _ => false);
 
-fun is_stale_typedef_abs ctxt whacks (s, T) =
+fun is_stale_typedef_abs ctxt (s, T) =
   (case T of
     Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
-    classify_type_name ctxt absT_name <> Typedef andalso
-    is_maybe_typedef_abs ctxt whacks absT_name s
+    classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_abs ctxt absT_name s
   | _ => false);
 
-fun is_stale_typedef_rep ctxt whacks (s, T) =
+fun is_stale_typedef_rep ctxt (s, T) =
   (case T of
     Type (@{type_name fun}, [Type (absT_name, _), _]) =>
-    classify_type_name ctxt absT_name <> Typedef andalso
-    is_maybe_typedef_rep ctxt whacks absT_name s
+    classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_rep ctxt absT_name s
   | _ => false);
 
 fun instantiate_constant_types_in_term ctxt csts target =
@@ -887,12 +879,12 @@
 
           fun consider_typedef_or_quotient itypedef_or_quotient tuple_of s =
             let
-              val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt whacks s;
+              val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s;
               val tyenv = Sign.typ_match thy (T0, T) Vartab.empty;
               val substT = Envir.subst_type tyenv;
               val subst = Envir.subst_term_types tyenv;
               val repT = substT repT0;
-              val wrt = subst (wrt0 ());
+              val wrt = preprocess_prop false ctxt whacks (subst wrt0);
               val abs = subst abs0;
               val rep = subst rep0;
             in
@@ -944,12 +936,11 @@
               (case t of
                 Const (x as (s, T)) =>
                 (if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse
-                    is_co_datatype_case ctxt x orelse is_quotient_abs ctxt whacks x orelse
-                    is_quotient_rep ctxt whacks x orelse is_typedef_abs ctxt whacks x orelse
-                    is_typedef_rep ctxt whacks x then
+                    is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse
+                    is_quotient_rep ctxt x orelse is_typedef_abs ctxt x orelse
+                    is_typedef_rep ctxt x then
                    (seens, problem)
-                 else if is_stale_typedef_abs ctxt whacks x orelse
-                     is_stale_typedef_rep ctxt whacks x then
+                 else if is_stale_typedef_abs ctxt x orelse is_stale_typedef_rep ctxt x then
                    raise UNSUPPORTED_FUNC t
                  else
                    (case spec_rules_of ctxt x of