# HG changeset patch
# User wenzelm
# Date 1296683304 -3600
# Node ID f69bb9077b02f97238f987252f438e73d69ded56
# Parent  afdbec23b92bbc99fe99580b0d05251ae78e864a
tuned odd conditional expression;

diff -r afdbec23b92b -r f69bb9077b02 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Feb 02 20:32:50 2011 +0100
+++ b/src/Pure/global_theory.ML	Wed Feb 02 22:48:24 2011 +0100
@@ -116,8 +116,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
-  |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
-  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
+  |> (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);
 
 fun name_thms pre official name xs =
   map (uncurry (name_thm pre official)) (name_multi name xs);