tuned;
authorwenzelm
Sun Jul 28 14:37:32 2019 +0200 (3 weeks ago ago)
changeset 70616dbb32c2d5c2c
parent 70615 6ec97dc6670e
child 70617 495881aadbff
tuned;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sun Jul 28 14:28:40 2019 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sun Jul 28 14:37:32 2019 +0200
     1.3 @@ -124,9 +124,9 @@
     1.4  
     1.5  fun name_thm No_Name_Flags _ thm = thm
     1.6    | name_thm (Name_Flags {pre, official}) name thm = thm
     1.7 -      |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
     1.8 +      |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
     1.9            Thm.name_derivation name
    1.10 -      |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
    1.11 +      |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
    1.12            Thm.put_name_hint name;
    1.13  
    1.14  end;