tuned;
authorwenzelm
Sun Jul 28 11:53:51 2019 +0200 (3 weeks ago ago)
changeset 70611198be2de1efa
parent 70610 78514368ec63
child 70612 973bf3e42e54
tuned;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sat Jul 27 21:47:43 2019 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sun Jul 28 11:53:51 2019 +0200
     1.3 @@ -112,10 +112,10 @@
     1.4    | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
     1.5  
     1.6  fun name_thm pre official name thm = thm
     1.7 -  |> (if not official orelse pre andalso Thm.derivation_name thm <> "" then I
     1.8 -      else Thm.name_derivation name)
     1.9 -  |> (if name = "" orelse pre andalso Thm.has_name_hint thm then I
    1.10 -      else Thm.put_name_hint name);
    1.11 +  |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
    1.12 +      Thm.name_derivation name
    1.13 +  |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
    1.14 +      Thm.put_name_hint name;
    1.15  
    1.16  fun name_thms pre official name thms =
    1.17    map (uncurry (name_thm pre official)) (name_multi name thms);