avoid duplicate mixfix messages in '(co)datatype' type name
authorblanchet
Mon, 25 Apr 2016 21:09:02 +0200
changeset 63048 1836456b7d82
parent 63047 2146553e96c6
child 63049 2cc4e85b46d4
avoid duplicate mixfix messages in '(co)datatype' type name
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;