src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 49672 902b24e0ffb4
parent 49671 61729b149397
child 49681 aa66ea552357
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 11:04:30 2012 +0200
     1.3 @@ -604,8 +604,8 @@
     1.4                    if s = s' then build_map (build_ctor_rec_arg mk_proj) T U else mk_proj T
     1.5                  | _ => mk_proj T);
     1.6  
     1.7 -            fun mk_U proj (T as Type (@{type_name prod}, [T', U])) =
     1.8 -                if member (op =) fpTs T' then proj (T', U) else T
     1.9 +            fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
    1.10 +                if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
    1.11                | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
    1.12                | mk_U _ T = T;
    1.13