--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jan 02 13:16:32 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jan 02 14:42:00 2018 +0100
@@ -376,7 +376,7 @@
|> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
|> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps)
|> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
- (*Ideally, this would only be issued if the "code" plugin is enabled.*)
+ (*Ideally, this would be issued only if the "code" plugin is enabled.*)
|> Local_Theory.notes notes;
val phi0 = substitute_noted_thm noted;
@@ -386,8 +386,8 @@
(fn phi => Data.map (@{fold 3} (fn T_name => fn Const (size_name, _) =>
fn overloaded_size_def =>
let val morph = Morphism.thm (phi0 $> phi) in
- Symtab.update (T_name, (size_name, (morph overloaded_size_def, map morph size_simps,
- maps (map morph) size_gen_o_map_thmss)))
+ Symtab.update (T_name, (size_name, (morph overloaded_size_def,
+ map morph overloaded_size_simps, maps (map morph) size_gen_o_map_thmss)))
end)
T_names size_consts overloaded_size_defs))
end