src/HOL/Tools/SMT/smt_datatypes.ML

         val binder_Ts = binder_types (fastype_of ctr)
       in
         mk_selectors T binder_Ts sels #>> pair ctr
       end
 
-    val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
+    val selss =
+      if has_duplicates (op aconv) (flat selss0) orelse
+         exists (exists (can (dest_funT o range_type o fastype_of))) selss0 then
+        []
+      else
+        selss0
   in
     @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
     |>> (pair T #> single)
   end