--- a/src/HOL/Analysis/measurable.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML Mon Aug 16 11:49:39 2021 +0200
@@ -53,8 +53,8 @@
preprocessors : (string * preprocessor) list }
val empty: T = {
measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
- dest_thms = Thm.full_rules,
- cong_thms = Thm.full_rules,
+ dest_thms = Thm.item_net,
+ cong_thms = Thm.item_net,
preprocessors = [] };
val extend = I;
fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
--- a/src/HOL/Eisbach/match_method.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML Mon Aug 16 11:49:39 2021 +0200
@@ -48,7 +48,7 @@
Scan.lift (\<^keyword>\<open>premises\<close> |-- Args.mode "local") >> Match_Prems ||
Scan.lift (\<^keyword>\<open>(\<close>) |-- Args.term --| Scan.lift (\<^keyword>\<open>)\<close>) >>
(fn t => Match_Term (Item_Net.update t aconv_net)) ||
- Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
+ Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.item_net));
fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false);
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Aug 16 11:49:39 2021 +0200
@@ -87,7 +87,7 @@
val empty =
{ quot_maps = Symtab.empty,
quotients = Symtab.empty,
- reflexivity_rules = Thm.full_rules,
+ reflexivity_rules = Thm.item_net,
relator_distr_data = Symtab.empty,
restore_data = Symtab.empty,
no_code_types = Symtab.empty
@@ -277,7 +277,7 @@
Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context
fun init_restore_data bundle_name qinfo context =
- update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } context
+ update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.item_net } context
fun add_transfer_rules_in_restore_data bundle_name transfer_rules context =
(case Symtab.lookup (get_restore_data' context) bundle_name of
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Aug 16 11:49:39 2021 +0200
@@ -1026,7 +1026,7 @@
val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
in
fn phi => fold_rev
- (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
+ (Item_Net.update o Morphism.thm phi) transfer_rules Thm.item_net
end
in
case Lifting_Info.lookup_restore_data lthy pointer of
--- a/src/HOL/Tools/Transfer/transfer.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Mon Aug 16 11:49:39 2021 +0200
@@ -94,13 +94,13 @@
relator_domain : thm Item_Net.T,
pred_data : pred_data Symtab.table }
val empty =
- { transfer_raw = Thm.intro_rules,
+ { transfer_raw = Thm.item_net_intro,
known_frees = [],
compound_lhs = compound_xhs_empty_net,
compound_rhs = compound_xhs_empty_net,
relator_eq = rewr_rules,
- relator_eq_raw = Thm.full_rules,
- relator_domain = Thm.full_rules,
+ relator_eq_raw = Thm.item_net,
+ relator_domain = Thm.item_net,
pred_data = Symtab.empty }
val extend = I
fun merge
--- a/src/Pure/Isar/calculation.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Aug 16 11:49:39 2021 +0200
@@ -33,7 +33,7 @@
structure Data = Generic_Data
(
type T = (thm Item_Net.T * thm Item_Net.T) * calculation option;
- val empty = ((Thm.elim_rules, Thm.full_rules), NONE);
+ val empty = ((Thm.item_net_elim, Thm.item_net), NONE);
val extend = I;
fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE);
--- a/src/Pure/Isar/class.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/Isar/class.ML Mon Aug 16 11:49:39 2021 +0200
@@ -227,7 +227,7 @@
make_class_data (((map o apply2) fst params, base_sort,
base_morph, export_morph, Option.map Thm.trim_context some_assm_intro,
Thm.trim_context of_class, Option.map Thm.trim_context some_axiom),
- (Thm.full_rules, operations)))
+ (Thm.item_net, operations)))
#> fold (curry Graph.add_edge class) sups;
in Class_Data.map add_class thy end;
--- a/src/Pure/Isar/locale.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/Isar/locale.ML Mon Aug 16 11:49:39 2021 +0200
@@ -669,7 +669,7 @@
structure Thms = Generic_Data
(
type T = thm Item_Net.T * thm Item_Net.T * thm Item_Net.T;
- val empty = (Thm.full_rules, Thm.full_rules, Thm.full_rules);
+ val empty = (Thm.item_net, Thm.item_net, Thm.item_net);
val extend = I;
fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
(Item_Net.merge (witnesses1, witnesses2),
--- a/src/Pure/Tools/named_theorems.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/Tools/named_theorems.ML Mon Aug 16 11:49:39 2021 +0200
@@ -34,7 +34,7 @@
Data.map (fn data =>
if Symtab.defined data name
then error ("Duplicate declaration of named theorems: " ^ quote name)
- else Symtab.update (name, Thm.full_rules) data);
+ else Symtab.update (name, Thm.item_net) data);
fun undeclared name = "Undeclared named theorems " ^ quote name;
@@ -58,7 +58,7 @@
val get = content o Context.Proof;
-fun clear name = map_entry name (K Thm.full_rules);
+fun clear name = map_entry name (K Thm.item_net);
fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
fun del_thm name = map_entry name o Item_Net.remove;
--- a/src/Pure/Tools/named_thms.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/Tools/named_thms.ML Mon Aug 16 11:49:39 2021 +0200
@@ -21,7 +21,7 @@
structure Data = Generic_Data
(
type T = thm Item_Net.T;
- val empty = Thm.full_rules;
+ val empty = Thm.item_net;
val extend = I;
val merge = Item_Net.merge;
);
--- a/src/Pure/more_thm.ML Mon Aug 16 11:24:12 2021 +0200
+++ b/src/Pure/more_thm.ML Mon Aug 16 11:49:39 2021 +0200
@@ -56,9 +56,9 @@
val add_thm: thm -> thm list -> thm list
val del_thm: thm -> thm list -> thm list
val merge_thms: thm list * thm list -> thm list
- val full_rules: thm Item_Net.T
- val intro_rules: thm Item_Net.T
- val elim_rules: thm Item_Net.T
+ val item_net: thm Item_Net.T
+ val item_net_intro: thm Item_Net.T
+ val item_net_elim: thm Item_Net.T
val declare_hyps: cterm -> Proof.context -> Proof.context
val assume_hyps: cterm -> Proof.context -> thm * Proof.context
val unchecked_hyps: Proof.context -> Proof.context
@@ -265,9 +265,9 @@
val del_thm = remove eq_thm_prop;
val merge_thms = merge eq_thm_prop;
-val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
-val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
-val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
+val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
+val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of);
+val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);