avoid accidental specialization of the types in the "map" property of codatatypes
authorblanchet
Tue Apr 23 17:46:12 2013 +0200 (2013-04-23)
changeset 517465af40820948b
parent 51745 a06a3c777add
child 51747 e4b5bebe5235
avoid accidental specialization of the types in the "map" property of codatatypes
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:15:44 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:46:12 2013 +0200
     1.3 @@ -516,8 +516,12 @@
     1.4              val nones = replicate live NONE;
     1.5  
     1.6              val ctor_cong =
     1.7 -              if lfp then Drule.dummy_thm
     1.8 -              else cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor)] arg_cong;
     1.9 +              if lfp then
    1.10 +                Drule.dummy_thm
    1.11 +              else
    1.12 +                let val ctor' = mk_ctor Bs ctor in
    1.13 +                  cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
    1.14 +                end;
    1.15  
    1.16              fun mk_cIn ify =
    1.17                certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo