# HG changeset patch
# User wenzelm
# Date 1752228271 -7200
# Node ID 53e56e6a67c3f27a5b1b6ac84614ef1d2a49cb52
# Parent  c3085510366ea11a6ed3f00cacb5616b8e129fd2
tuned: order does not matter here;

diff -r c3085510366e -r 53e56e6a67c3 src/Provers/classical.ML
--- 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);