# HG changeset patch
# User wenzelm
# Date 1564307631 -7200
# Node ID 198be2de1efaaf7645cfb2ba60e59f966c6b92e9
# Parent  78514368ec63217c65a1ab8542e093fe85a9682d
tuned;

diff -r 78514368ec63 -r 198be2de1efa src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Jul 27 21:47:43 2019 +0200
+++ b/src/Pure/global_theory.ML	Sun Jul 28 11:53:51 2019 +0200
@@ -112,10 +112,10 @@
   | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
 
 fun name_thm pre official name thm = thm
-  |> (if not official orelse pre andalso Thm.derivation_name thm <> "" then I
-      else Thm.name_derivation name)
-  |> (if name = "" orelse pre andalso Thm.has_name_hint thm then I
-      else Thm.put_name_hint name);
+  |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
+      Thm.name_derivation name
+  |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
+      Thm.put_name_hint name;
 
 fun name_thms pre official name thms =
   map (uncurry (name_thm pre official)) (name_multi name thms);