diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Sun Jun 09 15:31:33 2024 +0200 @@ -459,7 +459,7 @@ (*Use "theorem naming" to label the clauses*) fun name_thms label = let fun name1 th (k, ths) = - (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) + (k-1, Thm.put_name_hint (label ^ string_of_int k, 0) th :: ths) in fn ths => #2 (fold_rev name1 ths (length ths, [])) end; (*Is the given disjunction an all-negative support clause?*)