# HG changeset patch
# User wenzelm
# Date 1751724768 -7200
# Node ID 230eaf8d4f60b13388f081b126de22c67005c48e
# Parent  b908d50f42d409d7875ac29082267954ec4e3dd8
tuned signature: do not expose private operation;

diff -r b908d50f42d4 -r 230eaf8d4f60 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sat Jul 05 16:01:40 2025 +0200
+++ b/src/Pure/bires.ML	Sat Jul 05 16:12:48 2025 +0200
@@ -16,7 +16,6 @@
   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 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 -> rule list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
@@ -59,7 +58,9 @@
 
 
 (*delete one kbrl from the pair of nets*)
-fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
+local
+  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
+in
 
 fun delete_tagged_rule (brl as (eres, th)) (inet, enet) =
   (if eres then
@@ -71,6 +72,7 @@
 
 fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls;
 
+end;
 
 (*biresolution using a pair of nets rather than rules.
     function "order" must sort and possibly filter the list of brls.