src/HOL/Tools/SMT/smt_datatypes.ML
changeset 59142 705f8aea8d60
parent 59020 a86683d6c97e
child 59143 15c342a9a8e0
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Mon Dec 15 07:20:48 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Mon Dec 15 07:20:48 2014 +0100
     1.3 @@ -36,7 +36,12 @@
     1.4          mk_selectors T binder_Ts sels #>> pair ctr
     1.5        end
     1.6  
     1.7 -    val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
     1.8 +    val selss =
     1.9 +      if has_duplicates (op aconv) (flat selss0) orelse
    1.10 +         exists (exists (can (dest_funT o range_type o fastype_of))) selss0 then
    1.11 +        []
    1.12 +      else
    1.13 +        selss0
    1.14    in
    1.15      @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
    1.16      |>> (pair T #> single)