correctly apply type substitution before checking for function types
authorblanchet
Mon Dec 15 07:20:49 2014 +0100 (2014-12-15)
changeset 5914315c342a9a8e0
parent 59142 705f8aea8d60
child 59144 c9b75c03de3c
correctly apply type substitution before checking for function types
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:49 2014 +0100
     1.3 @@ -27,23 +27,21 @@
     1.4  
     1.5  fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
     1.6    let
     1.7 -    fun mk_constr ctr0 sels0 =
     1.8 -      let
     1.9 -        val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
    1.10 -        val ctr = Ctr_Sugar.mk_ctr Ts ctr0
    1.11 -        val binder_Ts = binder_types (fastype_of ctr)
    1.12 -      in
    1.13 -        mk_selectors T binder_Ts sels #>> pair ctr
    1.14 -      end
    1.15 +    val selss = map (map (Ctr_Sugar.mk_disc_or_sel Ts)) selss0
    1.16 +    val ctrs = map (Ctr_Sugar.mk_ctr Ts) ctrs0
    1.17 +
    1.18 +    fun mk_constr ctr sels =
    1.19 +      mk_selectors T (binder_types (fastype_of ctr)) sels #>> pair ctr
    1.20  
    1.21 -    val selss =
    1.22 -      if has_duplicates (op aconv) (flat selss0) orelse
    1.23 -         exists (exists (can (dest_funT o range_type o fastype_of))) selss0 then
    1.24 -        []
    1.25 -      else
    1.26 -        selss0
    1.27 +    val selss' =
    1.28 +      (if has_duplicates (op aconv) (flat selss) orelse
    1.29 +          exists (exists (can (dest_funT o range_type o fastype_of))) selss then
    1.30 +         []
    1.31 +       else
    1.32 +         selss)
    1.33 +      |> Ctr_Sugar_Util.pad_list [] (length ctrs)
    1.34    in
    1.35 -    @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
    1.36 +    @{fold_map 2} mk_constr ctrs selss' ctxt
    1.37      |>> (pair T #> single)
    1.38    end
    1.39