src/HOL/Tools/Meson/meson.ML
changeset 80306 c2537860ccf8
parent 77879 dd222e2af01a
--- 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?*)