tuned: order does not matter here;

--- a/src/Provers/classical.ML	Fri Jul 11 11:59:22 2025 +0200
+++ b/src/Provers/classical.ML	Fri Jul 11 12:04:31 2025 +0200
@@ -287,12 +287,12 @@
 
 (*Insert into netpair from next index, which is negative to give the
   new insertions the lowest priority.*)
-fun insert k = fold_rev Bires.insert_tagged_rule o (tag_brls (2 * k)) o joinrules;
+fun insert k = fold Bires.insert_tagged_rule o (tag_brls (2 * k)) o joinrules;
 
 fun insert_default_weight w0 w k =
-  fold_rev Bires.insert_tagged_rule o tag_weight_brls (the_default w0 w) k o single;
+  fold Bires.insert_tagged_rule o tag_weight_brls (the_default w0 w) k o single;
 
-fun delete x = fold_rev Bires.delete_tagged_rule (joinrules x);
+fun delete x = fold Bires.delete_tagged_rule (joinrules x);
 
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);