# HG changeset patch
# User blanchet
# Date 1418624448 -3600
# Node ID 705f8aea8d608ec252e73d68ca8b0c50254f5532
# Parent  9a5c2e9b001ea0e1b955eaff9f2db1dc56d4e532
avoid generating selectors with function types -- this produce arity inconsistencies

diff -r 9a5c2e9b001e -r 705f8aea8d60 src/HOL/Tools/SMT/smt_datatypes.ML
--- 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)