--- a/src/Pure/global_theory.ML Fri Aug 02 14:14:49 2019 +0200
+++ b/src/Pure/global_theory.ML Sat Aug 03 12:58:53 2019 +0200
@@ -122,12 +122,16 @@
val unofficial1 = Name_Flags {pre = true, official = false};
val unofficial2 = Name_Flags {pre = false, official = false};
-fun name_thm No_Name_Flags _ thm = thm
- | name_thm (Name_Flags {pre, official}) name thm = thm
- |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
- Thm.name_derivation name
- |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
- Thm.put_name_hint name;
+fun name_thm name_flags name =
+ Thm.solve_constraints #> (fn thm =>
+ (case name_flags of
+ No_Name_Flags => thm
+ | Name_Flags {pre, official} =>
+ thm
+ |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
+ Thm.name_derivation name
+ |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
+ Thm.put_name_hint name));
end;