tuned -- more uniform;

--- a/src/Pure/Isar/proof_context.ML	Wed Mar 07 17:27:57 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 07 17:39:18 2018 +0100
@@ -1077,7 +1077,8 @@
 fun add_thms_lazy kind (b, ths) ctxt =
   let
     val name = full_name ctxt b;
-    val ths' = Lazy.map (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind)) ths;
+    val ths' = ths
+      |> Lazy.map_finished (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind));
     val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
   in ctxt' end;
 

--- 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 =