# HG changeset patch
# User wenzelm
# Date 1629107379 -7200
# Node ID 069f6b2c5a077017d7e4429786242d39b3d1b745
# Parent  c3b3517ef4baa77be72872cb3423b38d5bc1ced8
tuned signature;

diff -r c3b3517ef4ba -r 069f6b2c5a07 src/HOL/Analysis/measurable.ML
--- 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 },
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/HOL/Eisbach/match_method.ML
--- 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);
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/HOL/Tools/Lifting/lifting_info.ML
--- 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
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/HOL/Tools/Transfer/transfer.ML
--- 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
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/Isar/calculation.ML
--- 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);
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/Isar/class.ML
--- 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;
 
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/Isar/locale.ML
--- 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),
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/Tools/named_theorems.ML
--- 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;
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/Tools/named_thms.ML
--- 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;
 );
diff -r c3b3517ef4ba -r 069f6b2c5a07 src/Pure/more_thm.ML
--- 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);