tuned signature;
authorwenzelm
Sun, 06 Jul 2025 11:43:34 +0200
changeset 82814 de15cf3e6325
parent 82813 b185d1441092
child 82815 cb0062a20be1
tuned signature;
src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Jul 06 11:35:18 2025 +0200
+++ b/src/Provers/classical.ML	Sun Jul 06 11:43:34 2025 +0200
@@ -263,17 +263,19 @@
   then rules added most recently (preferring the head of the list).*)
 fun tag_brls k [] = []
   | tag_brls k (brl::brls) =
-      ({weight = Bires.subgoals_of brl, index = k}, brl) ::
-      tag_brls (k+1) brls;
+      ({weight = Bires.subgoals_of brl, index = k}, brl) :: tag_brls (k + 1) brls;
 
-fun tag_brls' _ _ [] = []
-  | tag_brls' w k (brl::brls) = ({weight = w, index = k}, brl) :: tag_brls' w (k + 1) brls;
+fun tag_weight_brls _ _ [] = []
+  | tag_weight_brls w k (brl::brls) =
+      ({weight = w, index = k}, brl) :: tag_weight_brls w (k + 1) brls;
 
 (*Insert into netpair that already has nI intr rules and nE elim rules.
   Count the intr rules double (to account for swapify).  Negate to give the
   new insertions the lowest priority.*)
 fun insert (nI, nE) = Bires.insert_tagged_rules o (tag_brls (~(2*nI+nE))) o joinrules;
-fun insert' w (nI, nE) = Bires.insert_tagged_rules o tag_brls' w (~(nI + nE)) o joinrules;
+
+fun insert_default_weight w0 w (nI, nE) =
+  Bires.insert_tagged_rules o tag_weight_brls (the_default w0 w) (~(nI + nE)) o joinrules;
 
 fun delete x = Bires.delete_tagged_rules (joinrules x);
 
@@ -322,7 +324,7 @@
         uwrappers = uwrappers,
         unsafe_netpair = unsafe_netpair,
         dup_netpair = dup_netpair,
-        extra_netpair = insert' (the_default 0 w) (nI, nE) ([th], []) extra_netpair}
+        extra_netpair = insert_default_weight 0 w (nI, nE) ([th], []) extra_netpair}
     end;
 
 fun add_safe_elim w r
@@ -348,7 +350,7 @@
         uwrappers = uwrappers,
         unsafe_netpair = unsafe_netpair,
         dup_netpair = dup_netpair,
-        extra_netpair = insert' (the_default 0 w) (nI, nE) ([], [th]) extra_netpair}
+        extra_netpair = insert_default_weight 0 w (nI, nE) ([], [th]) extra_netpair}
     end;
 
 fun add_unsafe_intro w r
@@ -372,7 +374,7 @@
         uwrappers = uwrappers,
         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
-        extra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) extra_netpair}
+        extra_netpair = insert_default_weight 1 w (nI, nE) ([th], []) extra_netpair}
     end;
 
 fun add_unsafe_elim w r
@@ -396,7 +398,7 @@
         uwrappers = uwrappers,
         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
-        extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair}
+        extra_netpair = insert_default_weight 1 w (nI, nE) ([], [th]) extra_netpair}
     end;
 
 fun trim_context (th, (th1, ths1), (th2, ths2)) =