src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -1923,7 +1923,8 @@
       ||>> variant_tfrees fp_b_names;
 
     fun add_fake_type spec =
-      Typedecl.basic_typedecl true (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
+      Typedecl.basic_typedecl {final = true}
+        (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
 
     val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy;