avoid generating selectors with function types -- this produce arity inconsistencies
authorblanchet
Mon Dec 15 07:20:48 2014 +0100 (2014-12-15)
changeset 59142705f8aea8d60
parent 59141 9a5c2e9b001e
child 59143 15c342a9a8e0
avoid generating selectors with function types -- this produce arity inconsistencies
src/HOL/Tools/SMT/smt_datatypes.ML
     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)