--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jan 05 11:00:12 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jan 05 21:24:14 2015 +0100
@@ -1020,7 +1020,7 @@
|> map Thm.close_derivation)
end;
- val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
+ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
val anonymous_notes =
[(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
@@ -1455,7 +1455,7 @@
val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
- val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
+ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
in
((induct_thms, induct_thm, mk_induct_attrs ctrss),
(rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
@@ -2081,7 +2081,7 @@
val fpTs = map (domain_type o fastype_of) dtors;
val fpBTs = map B_ify_T fpTs;
- val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
+ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
val ns = map length ctr_Tsss;