src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

       ||>> mk_TFrees nn
       ||>> mk_TFrees nn
       ||>> 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;
 
     val qsoty = quote o Syntax.string_of_typ fake_lthy;