--- 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,