# HG changeset patch
# User blanchet
# Date 1514900520 -3600
# Node ID 315b5c29e9270ec9f3b9d36ed519a9ed7896566f
# Parent  a2d7c0987f1987fdd042d51320df83abd7491d64
store high-level 'size' equations

diff -r a2d7c0987f19 -r 315b5c29e927 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- 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