# HG changeset patch
# User blanchet
# Date 1461611342 -7200
# Node ID 1836456b7d8279fbf786a475b77a2b680ef6b015
# Parent  2146553e96c6fbb839aa8454cdce73e3405bcf63
avoid duplicate mixfix messages in '(co)datatype' type name

diff -r 2146553e96c6 -r 1836456b7d82 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 25 19:23:20 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 25 21:09:02 2016 +0200
@@ -2057,7 +2057,7 @@
 
     fun add_fake_type spec =
       Typedecl.basic_typedecl {final = true}
-        (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
+        (type_binding_of_spec spec, num_As, Mixfix.reset_pos (mixfix_of_spec spec));
 
     val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy;