tuned signature: more explicit types;

--- a/src/Provers/classical.ML	Sat Jul 05 14:19:45 2025 +0200
+++ b/src/Provers/classical.ML	Sat Jul 05 14:39:24 2025 +0200
@@ -97,7 +97,7 @@
   include BASIC_CLASSICAL
   val classical_rule: Proof.context -> thm -> thm
   type rule = thm * (thm * thm list) * (thm * thm list)
-  type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
+  type netpair = int Bires.netpair
   val rep_cs: claset ->
    {safeIs: rule Item_Net.T,
     safeEs: rule Item_Net.T,
@@ -217,7 +217,7 @@
 type rule = thm * (thm * thm list) * (thm * thm list);
   (*external form, internal form (possibly swapped), dup form (possibly swapped)*)
 
-type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
+type netpair = int Bires.netpair;
 type wrapper = (int -> tactic) -> int -> tactic;
 
 datatype claset =

--- a/src/Pure/Isar/context_rules.ML	Sat Jul 05 14:19:45 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Jul 05 14:39:24 2025 +0200
@@ -7,7 +7,7 @@
 
 signature CONTEXT_RULES =
 sig
-  type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net
+  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
@@ -61,7 +61,7 @@
 
 (* context data *)
 
-type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
+type netpair = (int * int) Bires.netpair;
 val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
 
 datatype rules = Rules of

--- a/src/Pure/bires.ML	Sat Jul 05 14:19:45 2025 +0200
+++ b/src/Pure/bires.ML	Sat Jul 05 14:39:24 2025 +0200
@@ -1,25 +1,22 @@
 (*  Title:      Pure/bires.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Makarius
 
 Biresolution and resolution using nets.
 *)
 
 signature BIRES =
 sig
-  val insert_tagged_brl: 'a * (bool * thm) ->
-    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
-      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
-  val delete_tagged_brl: bool * thm ->
-    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
-      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
-  val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
+  type rule = bool * thm
+  type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net;
+  val insert_tagged_brl: 'a * rule -> 'a netpair -> 'a netpair
+  val delete_tagged_brl: rule -> 'a netpair -> 'a netpair
+  val eq_kbrl: ('a * rule) * ('a * rule) -> bool
   val build_net: thm list -> (int * thm) Net.net
   val biresolution_from_nets_tac: Proof.context ->
-    ('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
-  val biresolve_from_nets_tac: Proof.context ->
-    (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
-  val bimatch_from_nets_tac: Proof.context ->
-    (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
+    ('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
   val filt_resolve_from_net_tac: Proof.context -> int -> (int * thm) Net.net -> int -> tactic
   val resolve_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
   val match_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
@@ -28,6 +25,11 @@
 structure Bires: BIRES =
 struct
 
+type rule = bool * thm;  (*eres flag, see Thm.biresolution*)
+
+type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net;
+
+
 (** To preserve the order of the rules, tag them with increasing integers **)
 
 (*insert one tagged brl into the pair of nets*)