just one type Bires.netpair, based on Bires.tag with explicit weight;
more general order_list operations;

--- a/src/Provers/blast.ML	Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Provers/blast.ML	Sun Jul 06 11:33:23 2025 +0200
@@ -566,18 +566,18 @@
   | isVarForm (Const (c, _) $ Var _) = (c = Data.not_name)
   | isVarForm _ = false;
 
-fun netMkRules state P vars (nps: Classical.netpair list) =
+fun netMkRules state P vars (nps: Bires.netpair list) =
   case P of
       (Const ("*Goal*", _) $ G) =>
         let val pG = mk_Trueprop (toTerm 2 G)
             val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
-        in  map (fromIntrRule state vars o #2) (order_list intrs)  end
+        in  map (fromIntrRule state vars o #2) (Bires.tag_order intrs)  end
     | _ =>
         if isVarForm P then [] (*The formula is too flexible, reject*)
         else
         let val pP = mk_Trueprop (toTerm 3 P)
             val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
-        in  map_filter (fromRule state vars o #2) (order_list elims)  end;
+        in  map_filter (fromRule state vars o #2) (Bires.tag_order elims)  end;
 
 
 (*Normalize a branch--for tracing*)

--- a/src/Provers/classical.ML	Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Provers/classical.ML	Sun Jul 06 11:33:23 2025 +0200
@@ -97,7 +97,6 @@
   include BASIC_CLASSICAL
   val classical_rule: Proof.context -> thm -> thm
   type rule = thm * (thm * thm list) * (thm * thm list)
-  type netpair = int Bires.netpair
   val rep_cs: claset ->
    {safeIs: rule Item_Net.T,
     safeEs: rule Item_Net.T,
@@ -105,11 +104,11 @@
     unsafeEs: rule Item_Net.T,
     swrappers: (string * (Proof.context -> wrapper)) list,
     uwrappers: (string * (Proof.context -> wrapper)) list,
-    safe0_netpair: netpair,
-    safep_netpair: netpair,
-    unsafe_netpair: netpair,
-    dup_netpair: netpair,
-    extra_netpair: Context_Rules.netpair}
+    safe0_netpair: Bires.netpair,
+    safep_netpair: Bires.netpair,
+    unsafe_netpair: Bires.netpair,
+    dup_netpair: Bires.netpair,
+    extra_netpair: Bires.netpair}
   val get_cs: Context.generic -> claset
   val map_cs: (claset -> claset) -> Context.generic -> Context.generic
   val safe_dest: int option -> attribute
@@ -217,7 +216,6 @@
 type rule = thm * (thm * thm list) * (thm * thm list);
   (*external form, internal form (possibly swapped), dup form (possibly swapped)*)
 
-type netpair = int Bires.netpair;
 type wrapper = (int -> tactic) -> int -> tactic;
 
 datatype claset =
@@ -228,17 +226,15 @@
     unsafeEs: rule Item_Net.T,  (*unsafe elimination rules*)
     swrappers: (string * (Proof.context -> wrapper)) list,  (*for transforming safe_step_tac*)
     uwrappers: (string * (Proof.context -> wrapper)) list,  (*for transforming step_tac*)
-    safe0_netpair: netpair,  (*nets for trivial cases*)
-    safep_netpair: netpair,  (*nets for >0 subgoals*)
-    unsafe_netpair: netpair,  (*nets for unsafe rules*)
-    dup_netpair: netpair,  (*nets for duplication*)
-    extra_netpair: Context_Rules.netpair};  (*nets for extra rules*)
+    safe0_netpair: Bires.netpair,  (*nets for trivial cases*)
+    safep_netpair: Bires.netpair,  (*nets for >0 subgoals*)
+    unsafe_netpair: Bires.netpair,  (*nets for unsafe rules*)
+    dup_netpair: Bires.netpair,  (*nets for duplication*)
+    extra_netpair: Bires.netpair};  (*nets for extra rules*)
 
 val empty_rules: rule Item_Net.T =
   Item_Net.init (Thm.eq_thm_prop o apply2 #1) (single o Thm.full_prop_of o #1);
 
-val empty_netpair = (Net.empty, Net.empty);
-
 val empty_cs =
   CS
    {safeIs = empty_rules,
@@ -247,11 +243,11 @@
     unsafeEs = empty_rules,
     swrappers = [],
     uwrappers = [],
-    safe0_netpair = empty_netpair,
-    safep_netpair = empty_netpair,
-    unsafe_netpair = empty_netpair,
-    dup_netpair = empty_netpair,
-    extra_netpair = empty_netpair};
+    safe0_netpair = Bires.empty_netpair,
+    safep_netpair = Bires.empty_netpair,
+    unsafe_netpair = Bires.empty_netpair,
+    dup_netpair = Bires.empty_netpair,
+    extra_netpair = Bires.empty_netpair};
 
 fun rep_cs (CS args) = args;
 
@@ -267,11 +263,11 @@
   then rules added most recently (preferring the head of the list).*)
 fun tag_brls k [] = []
   | tag_brls k (brl::brls) =
-      (1000000*Bires.subgoals_of brl + k, brl) ::
+      ({weight = 0, index = 1000000*Bires.subgoals_of brl + k}, brl) ::
       tag_brls (k+1) brls;
 
 fun tag_brls' _ _ [] = []
-  | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
+  | tag_brls' w k (brl::brls) = ({weight = w, index = k}, brl) :: tag_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
@@ -736,8 +732,8 @@
 (*version of Bires.bimatch_from_nets_tac that only applies rules that
   create precisely n subgoals.*)
 fun n_bimatch_from_nets_tac ctxt n =
-  Bires.biresolution_from_nets_tac ctxt
-    (order_list o filter (fn (_, rl) => Bires.subgoals_of rl = n)) true;
+  Bires.biresolution_from_nets_tac ctxt Bires.tag_ord
+    (SOME (fn rl => Bires.subgoals_of rl = n)) true;
 
 fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
 fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;

--- a/src/Pure/Isar/context_rules.ML	Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sun Jul 06 11:33:23 2025 +0200
@@ -7,11 +7,9 @@
 
 signature CONTEXT_RULES =
 sig
-  type netpair = (int * int) Bires.netpair
-  val netpair_bang: Proof.context -> netpair
-  val netpair: Proof.context -> netpair
-  val orderlist: ((int * int) * 'a) list -> 'a list
-  val find_rules_netpair: Proof.context -> bool -> thm list -> term -> netpair -> thm list
+  val netpair_bang: Proof.context -> Bires.netpair
+  val netpair: Proof.context -> Bires.netpair
+  val find_rules_netpair: Proof.context -> bool -> thm list -> term -> Bires.netpair -> thm list
   val find_rules: Proof.context -> bool -> thm list -> term -> thm list list
   val print_rules: Proof.context -> unit
   val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
@@ -61,13 +59,13 @@
 
 (* context data *)
 
-type netpair = (int * int) Bires.netpair;
-val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
+val empty_netpairs: Bires.netpair list =
+  replicate (length rule_indexes) Bires.empty_netpair;
 
 datatype rules = Rules of
  {next: int,
   rules: (int * ((int * bool) * thm)) list,
-  netpairs: netpair list,
+  netpairs: Bires.netpair list,
   wrappers:
     ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
     ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list};
@@ -75,13 +73,14 @@
 fun make_rules next rules netpairs wrappers =
   Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
 
-fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
+fun add_rule (i, b) opt_weight th (Rules {next, rules, netpairs, wrappers}) =
   let
-    val w = opt_w |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
+    val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
+    val tag = {weight = weight, index = next};
     val th' = Thm.trim_context th;
   in
-    make_rules (next - 1) ((w, ((i, b), th')) :: rules)
-      (nth_map i (Bires.insert_tagged_rule ((w, next), (b, th'))) netpairs) wrappers
+    make_rules (next - 1) ((weight, ((i, b), th')) :: rules)
+      (nth_map i (Bires.insert_tagged_rule (tag, (b, th'))) netpairs) wrappers
   end;
 
 fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
@@ -108,8 +107,8 @@
       val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
           k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
       val next = ~ (length rules);
-      val netpairs = fold (fn (n, (w, ((i, b), th))) =>
-          nth_map i (Bires.insert_tagged_rule ((w, n), (b, th))))
+      val netpairs = fold (fn (index, (weight, ((i, b), th))) =>
+          nth_map i (Bires.insert_tagged_rule ({weight = weight, index = index}, (b, th))))
         (next upto ~1 ~~ rules) empty_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end;
 );
@@ -134,22 +133,13 @@
 
 (* retrieving rules *)
 
-fun untaglist [] = []
-  | untaglist [(_ : int * int, x)] = [x]
-  | untaglist ((k, x) :: (rest as (k', _) :: _)) =
-      if k = k' then untaglist rest
-      else x :: untaglist rest;
-
-fun orderlist brls =
-  untaglist (sort (prod_ord int_ord int_ord o apply2 fst) brls);
-
-fun orderlist_no_weight brls =
-  untaglist (sort (int_ord o apply2 (snd o fst)) brls);
-
 local
 
+fun order weighted =
+  make_order_list (Bires.weighted_tag_ord weighted) NONE;
+
 fun may_unify weighted t net =
-  map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
+  map snd (order weighted (Net.unify_term net t));
 
 fun find_erules _ [] = K []
   | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact));

--- a/src/Pure/bires.ML	Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Pure/bires.ML	Sun Jul 06 11:33:23 2025 +0200
@@ -8,18 +8,27 @@
 signature BIRES =
 sig
   type rule = bool * thm
-  type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net;
   val subgoals_of: rule -> int
   val subgoals_ord: rule ord
   val no_subgoals: rule -> bool
-  val insert_tagged_rule: 'a * rule -> 'a netpair -> 'a netpair
-  val insert_tagged_rules: ('a * rule) list -> 'a netpair -> 'a netpair
-  val delete_tagged_rule: rule -> 'a netpair -> 'a netpair
-  val delete_tagged_rules: rule list -> 'a netpair -> 'a netpair
-  val biresolution_from_nets_tac: Proof.context ->
-    ('a list -> rule list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
-  val biresolve_from_nets_tac: Proof.context -> int netpair -> int -> tactic
-  val bimatch_from_nets_tac: Proof.context -> int netpair -> int -> tactic
+
+  type tag = {weight: int, index: int}
+  val tag0_ord: tag ord
+  val tag_ord: tag ord
+  val weighted_tag_ord: bool -> tag ord
+  val tag_order: (tag * 'a) list -> 'a list
+
+  type netpair = (tag * rule) Net.net * (tag * rule) Net.net
+  val empty_netpair: netpair
+
+  val insert_tagged_rule: tag * rule -> netpair -> netpair
+  val insert_tagged_rules: (tag * rule) list -> netpair -> netpair
+  val delete_tagged_rule: rule -> netpair -> netpair
+  val delete_tagged_rules: rule list -> netpair -> netpair
+  val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option ->
+    bool -> netpair -> int -> tactic
+  val biresolve_from_nets_tac: Proof.context -> netpair -> int -> tactic
+  val bimatch_from_nets_tac: Proof.context -> netpair -> int -> tactic
 
   type net = (int * thm) Net.net
   val build_net: thm list -> net
@@ -33,9 +42,9 @@
 
 (** Natural Deduction using (bires_flg, rule) pairs **)
 
-type rule = bool * thm;  (*see Thm.biresolution*)
+(* type rule *)
 
-type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net;
+type rule = bool * thm;  (*see Thm.biresolution*)
 
 fun subgoals_of (true, thm) = Thm.nprems_of thm - 1
   | subgoals_of (false, thm) = Thm.nprems_of thm;
@@ -46,15 +55,34 @@
   | no_subgoals (false, thm) = Thm.no_prems thm;
 
 
+(* tagged rules *)
+
+type tag = {weight: int, index: int};
+
+val tag0_ord: tag ord = int_ord o apply2 #index;
+val tag_ord: tag ord = int_ord o apply2 #weight ||| tag0_ord;
+
+fun weighted_tag_ord weighted = if weighted then tag_ord else tag0_ord;
+
+fun tag_order list = make_order_list tag_ord NONE list;
+
+
+(* discrimination nets for intr/elim rules *)
+
+type netpair = (tag * rule) Net.net * (tag * rule) Net.net;
+
+val empty_netpair: netpair = (Net.empty, Net.empty);
+
+
 (** To preserve the order of the rules, tag them with increasing integers **)
 
 (*insert one tagged brl into the pair of nets*)
-fun insert_tagged_rule (kbrl as (k, (eres, th))) (inet, enet) =
+fun insert_tagged_rule (tagged_rule as (_, (eres, th))) ((inet, enet): netpair) =
   if eres then
     (case try Thm.major_prem_of th of
-      SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
+      SOME prem => (inet, Net.insert_term (K false) (prem, tagged_rule) enet)
     | NONE => error "insert_tagged_rule: elimination rule with no premises")
-  else (Net.insert_term (K false) (Thm.concl_of th, kbrl) inet, enet);
+  else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet);
 
 fun insert_tagged_rules rls = fold_rev insert_tagged_rule rls;
 
@@ -64,7 +92,7 @@
   fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
 in
 
-fun delete_tagged_rule (brl as (eres, th)) (inet, enet) =
+fun delete_tagged_rule (brl as (eres, th)) ((inet, enet): netpair) =
   (if eres then
     (case try Thm.major_prem_of th of
       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
@@ -76,21 +104,21 @@
 
 end;
 
-(*biresolution using a pair of nets rather than rules.
-    function "order" must sort and possibly filter the list of brls.
-    boolean "match" indicates matching or unification.*)
-fun biresolution_from_nets_tac ctxt order match (inet, enet) =
+(*biresolution using a pair of nets rather than rules:
+   boolean "match" indicates matching or unification.*)
+fun biresolution_from_nets_tac ctxt ord pred match ((inet, enet): netpair) =
   SUBGOAL
     (fn (prem, i) =>
       let
         val hyps = Logic.strip_assums_hyp prem;
         val concl = Logic.strip_assums_concl prem;
-        val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
-      in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order kbrls) i) end);
+        val tagged_rules = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
+        val order = make_order_list ord pred;
+      in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order tagged_rules) i) end);
 
 (*versions taking pre-built nets.  No filtering of brls*)
-fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list false;
-fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list true;
+fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE false;
+fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE true;
 
 
 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)

--- a/src/Pure/library.ML	Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Pure/library.ML	Sun Jul 06 11:33:23 2025 +0200
@@ -219,7 +219,8 @@
   val sort_strings: string list -> string list
   val sort_by: ('a -> string) -> 'a list -> 'a list
   val tag_list: int -> 'a list -> (int * 'a) list
-  val untag_list: (int * 'a) list -> 'a list
+  val untag_list: (''tag * 'a) list -> 'a list
+  val make_order_list: ''tag ord -> ('a -> bool) option -> (''tag * 'a) list -> 'a list
   val order_list: (int * 'a) list -> 'a list
 
   (*misc*)
@@ -1047,13 +1048,18 @@
 
 (*remove tags and suppress duplicates -- list is assumed sorted!*)
 fun untag_list [] = []
-  | untag_list [(k: int, x)] = [x]
-  | untag_list ((k, x) :: (rest as (k', x') :: _)) =
-      if k = k' then untag_list rest
+  | untag_list [(_, x)] = [x]
+  | untag_list ((tag, x) :: (rest as (tag', _) :: _)) =
+      if tag = tag' then untag_list rest
       else x :: untag_list rest;
 
-(*return list elements in original order*)
-fun order_list list = untag_list (sort (int_ord o apply2 fst) list);
+fun make_order_list ord pred list =
+  list
+  |> (case pred of NONE => I | SOME p => filter (p o snd))
+  |> sort (ord o apply2 fst)
+  |> untag_list;
+
+fun order_list list = make_order_list int_ord NONE list;
 
 
 

--- a/src/Tools/intuitionistic.ML	Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Tools/intuitionistic.ML	Sun Jul 06 11:33:23 2025 +0200
@@ -25,7 +25,7 @@
 
 fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
 
-fun bires_tac ctxt = Bires.biresolution_from_nets_tac ctxt Context_Rules.orderlist;
+fun bires_tac ctxt = Bires.biresolution_from_nets_tac ctxt Bires.tag_ord NONE;
 
 fun safe_step_tac ctxt =
   Context_Rules.Swrap ctxt