changeset 63239 | d562c9948dee |
parent 63222 | fe92356ade42 |
child 63859 | dca6fabd8060 |
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Jun 06 21:28:46 2016 +0200 @@ -354,7 +354,7 @@ end; (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *) - val code_attrs = Code.add_default_eqn_attrib; + val code_attrs = Code.add_default_eqn_attrib Code.Equation; val massage_multi_notes = maps (fn (thmN, thmss, attrs) =>