# HG changeset patch
# User wenzelm
# Date 1751969400 -7200
# Node ID 05d2b8b675dad8f6ac77489527c4814d1ccdfec5
# Parent  b7c1c23058cf157082bba7aaf9aa13c32454d597
clarified signature;

diff -r b7c1c23058cf -r 05d2b8b675da src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Jul 08 12:06:21 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue Jul 08 12:10:00 2025 +0200
@@ -73,7 +73,7 @@
 structure Data = Generic_Data
 (
   type T = rules;
-  val empty = make_rules Bires.empty_decls Bires.kind_netpairs ([], []);
+  val empty = make_rules Bires.empty_decls (Bires.kind_values Bires.empty_netpair) ([], []);
   fun merge
     (Rules {decls = decls1, netpairs = netpairs1, wrappers = (ws1, ws1')},
      Rules {decls = decls2, netpairs = _, wrappers = (ws2, ws2')}) =
diff -r b7c1c23058cf -r 05d2b8b675da src/Pure/bires.ML
--- a/src/Pure/bires.ML	Tue Jul 08 12:06:21 2025 +0200
+++ b/src/Pure/bires.ML	Tue Jul 08 12:10:00 2025 +0200
@@ -30,6 +30,7 @@
   val kind_index: kind -> int
   val kind_elim: kind -> bool
   val kind_domain: kind list
+  val kind_values: 'a -> 'a list
   val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list
   val kind_rule: kind -> thm -> rule
   val kind_title: kind -> string
@@ -47,7 +48,6 @@
 
   type netpair = (tag * rule) Net.net * (tag * rule) Net.net
   val empty_netpair: netpair
-  val kind_netpairs: netpair list
   val insert_tagged_rule: tag * rule -> netpair -> netpair
   val insert_tagged_rules: (tag * rule) list -> netpair -> netpair
   val delete_tagged_rule: rule -> netpair -> netpair
@@ -127,6 +127,9 @@
 
 val kind_domain = map #1 kind_infos;
 
+fun kind_values x =
+  replicate (length (distinct (op =) (map kind_index kind_domain))) x;
+
 fun kind_map kind f = nth_map (kind_index kind) f;
 fun kind_rule kind thm : rule = (kind_elim kind, thm);
 
@@ -204,9 +207,6 @@
 
 val empty_netpair: netpair = (Net.empty, Net.empty);
 
-val kind_netpairs =
-  replicate (length (distinct (op =) (map kind_index kind_domain))) empty_netpair;
-
 
 (** Natural Deduction using (bires_flg, rule) pairs **)