src/Provers/classical.ML

   | tag_weight_brls w k (brl::brls) =
       ({weight = w, index = k}, brl) :: tag_weight_brls w (k + 1) brls;
 
 (*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;
-
-fun delete x = fold_rev Bires.delete_tagged_rule (joinrules x);
+  fold Bires.insert_tagged_rule o tag_weight_brls (the_default w0 w) k o single;
+
+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);
 
 fun make_elim ctxt th =
   if Thm.no_prems th then bad_thm ctxt "Ill-formed destruction rule" th