# HG changeset patch
# User wenzelm
# Date 1564317452 -7200
# Node ID dbb32c2d5c2c1a2a6484e0ad51a83e81ebe86d98
# Parent  6ec97dc6670e83462c280e2886cba2dd5d4f8304
tuned;

diff -r 6ec97dc6670e -r dbb32c2d5c2c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Jul 28 14:28:40 2019 +0200
+++ b/src/Pure/global_theory.ML	Sun Jul 28 14:37:32 2019 +0200
@@ -124,9 +124,9 @@
 
 fun name_thm No_Name_Flags _ thm = thm
   | name_thm (Name_Flags {pre, official}) name thm = thm
-      |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
+      |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
           Thm.name_derivation name
-      |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
+      |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
           Thm.put_name_hint name;
 
 end;