# HG changeset patch
# User wenzelm
# Date 1751794518 -7200
# Node ID b185d1441092ff2f90f8dc065d7909421cca1e01
# Parent  ea8d633fd4a895f017e903c151674aa439d5f6fa
proper weight, instead of magic number 1000000 (see b3f190995bc9);

diff -r ea8d633fd4a8 -r b185d1441092 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Jul 06 11:33:23 2025 +0200
+++ b/src/Provers/classical.ML	Sun Jul 06 11:35:18 2025 +0200
@@ -263,7 +263,7 @@
   then rules added most recently (preferring the head of the list).*)
 fun tag_brls k [] = []
   | tag_brls k (brl::brls) =
-      ({weight = 0, index = 1000000*Bires.subgoals_of brl + k}, brl) ::
+      ({weight = Bires.subgoals_of brl, index = k}, brl) ::
       tag_brls (k+1) brls;
 
 fun tag_brls' _ _ [] = []