avoid generating selectors with function types -- this produce arity inconsistencies

--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Mon Dec 15 07:20:48 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Mon Dec 15 07:20:48 2014 +0100
@@ -36,7 +36,12 @@
         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)