diff -r a25f9076a0b3 -r fd2558014196 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Wed Mar 07 17:27:57 2018 +0100 +++ b/src/Pure/global_theory.ML Wed Mar 07 17:39:18 2018 +0100 @@ -136,7 +136,8 @@ else let val name = Sign.full_name thy b; - val thms' = Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind)) thms; + val thms' = thms + |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind)); in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end; fun enter_thms pre_name post_name app_att (b, thms) thy =