Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid accidental specialization of the types in the "map" property of codatatypes
authorblanchet
Tue, 23 Apr 2013 17:46:12 +0200
changeset 51746 5af40820948b
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 file | annotate | diff | comparison | revisions 
--- 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
isabelle