# HG changeset patch
# User blanchet
# Date 1366731972 -7200
# Node ID 5af40820948bc296130bfb637a90d2fdc1123dbf
# Parent  a06a3c777addb0a439df42789804bc1228dec093
avoid accidental specialization of the types in the "map" property of codatatypes

diff -r a06a3c777add -r 5af40820948b src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:15:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:46:12 2013 +0200
@@ -516,8 +516,12 @@
             val nones = replicate live NONE;
 
             val ctor_cong =
-              if lfp then Drule.dummy_thm
-              else cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor)] arg_cong;
+              if lfp then
+                Drule.dummy_thm
+              else
+                let val ctor' = mk_ctor Bs ctor in
+                  cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
+                end;
 
             fun mk_cIn ify =
               certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo