tuned signature;

--- a/src/Pure/Isar/spec_rules.ML	Mon May 15 14:21:00 2023 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Mon May 15 14:34:38 2023 +0200
@@ -117,7 +117,7 @@
   {pos = pos, name = name, rough_classification = rough_classification, terms = terms,
     rules = map f rules};
 
-structure Rules = Generic_Data
+structure Data = Generic_Data
 (
   type T = spec_rule Item_Net.T;
   val empty : T = Item_Net.init eq_spec #terms;
@@ -132,9 +132,9 @@
     val thy = Context.theory_of context;
     val transfer = Global_Theory.transfer_theories thy;
     fun imported spec =
-      imports |> exists (fn thy => Item_Net.member (Rules.get (Context.Theory thy)) spec);
+      imports |> exists (fn thy => Item_Net.member (Data.get (Context.Theory thy)) spec);
   in
-    Item_Net.content (Rules.get context)
+    Item_Net.content (Data.get context)
     |> filter_out imported
     |> (map o map_spec_rules) transfer
   end;
@@ -148,7 +148,7 @@
 (* retrieve *)
 
 fun retrieve_generic context =
-  Item_Net.retrieve (Rules.get context)
+  Item_Net.retrieve (Data.get context)
   #> (map o map_spec_rules) (Thm.transfer'' context);
 
 val retrieve = retrieve_generic o Context.Proof;
@@ -171,14 +171,14 @@
             |>> map (Thm.term_of o Drule.dest_term)
             ||> map Thm.trim_context;
         in
-          context |> (Rules.map o Item_Net.update)
+          context |> (Data.map o Item_Net.update)
             {pos = pos, name = name, rough_classification = rough_classification,
               terms = terms', rules = rules'}
         end)
   end;
 
 fun add_global b rough_classification terms rules thy =
-  thy |> (Context.theory_map o Rules.map o Item_Net.update)
+  thy |> (Context.theory_map o Data.map o Item_Net.update)
    {pos = Position.thread_data (),
     name = Sign.full_name thy b,
     rough_classification = rough_classification,