# HG changeset patch
# User desharna
# Date 1629148021 -7200
# Node ID 62b0577123a57f52ac43fcb8d86441b9fde0e255
# Parent  46f66e821f5c958c6d5b8ce337c8ed059ca2e857# Parent  069f6b2c5a077017d7e4429786242d39b3d1b745
merged

diff -r 46f66e821f5c -r 62b0577123a5 src/HOL/Analysis/measurable.ML
--- a/src/HOL/Analysis/measurable.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Aug 16 23:07:01 2021 +0200
@@ -32,23 +32,22 @@
 
 structure Data = Generic_Data
 (
-  type T = (thm Item_Net.T * thm list) * calculation option;
-  val empty = ((Thm.elim_rules, []), NONE);
+  type T = (thm Item_Net.T * thm Item_Net.T) * calculation option;
+  val empty = ((Thm.item_net_elim, Thm.item_net), NONE);
   val extend = I;
   fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
-    ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
+    ((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE);
 );
 
 val get_rules = #1 o Data.get o Context.Proof;
+val get_trans_rules = Item_Net.content o #1 o get_rules;
+val get_sym_rules = Item_Net.content o #2 o get_rules;
 val get_calculation = #2 o Data.get o Context.Proof;
 
 fun print_rules ctxt =
-  let
-    val pretty_thm = Thm.pretty_thm_item ctxt;
-    val (trans, sym) = get_rules ctxt;
-  in
-   [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
-    Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
+  let val pretty_thm = Thm.pretty_thm_item ctxt in
+   [Pretty.big_list "transitivity rules:" (map pretty_thm (get_trans_rules ctxt)),
+    Pretty.big_list "symmetry rules:" (map pretty_thm (get_sym_rules ctxt))]
   end |> Pretty.writeln_chunks;
 
 
@@ -106,12 +105,12 @@
 
 val sym_add =
   Thm.declaration_attribute (fn th =>
-    (Data.map o apfst o apsnd) (Thm.add_thm (Thm.trim_context th)) #>
+    (Data.map o apfst o apsnd) (Item_Net.update (Thm.trim_context th)) #>
     Thm.attribute_declaration (Context_Rules.elim_query NONE) th);
 
 val sym_del =
   Thm.declaration_attribute (fn th =>
-    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
+    (Data.map o apfst o apsnd) (Item_Net.remove th) #>
     Thm.attribute_declaration Context_Rules.rule_del th);
 
 
@@ -119,11 +118,12 @@
 
 val symmetric =
   Thm.rule_attribute [] (fn context => fn th =>
-    (case Seq.chop 2
-        (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
-      ([th'], _) => Drule.zero_var_indexes th'
-    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
-    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
+    let val ctxt = Context.proof_of context in
+      (case Seq.chop 2 (Drule.multi_resolves (SOME ctxt) [th] (get_sym_rules ctxt)) of
+        ([th'], _) => Drule.zero_var_indexes th'
+      | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
+      | _ => raise THM ("symmetric: multiple unifiers", 1, [th]))
+    end);
 
 
 (* concrete syntax *)
diff -r 46f66e821f5c -r 62b0577123a5 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Isar/class.ML	Mon Aug 16 23:07:01 2021 +0200
@@ -76,7 +76,7 @@
   axiom: thm option,
 
   (* dynamic part *)
-  defs: thm list,
+  defs: thm Item_Net.T,
   operations: (string * (class * ((typ * term) * bool))) list
 
   (* n.b.
@@ -102,7 +102,7 @@
   Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
     of_class = _, axiom = _, defs = defs2, operations = operations2}) =
   make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
-    (Thm.merge_thms (defs1, defs2),
+    (Item_Net.merge (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
 structure Class_Data = Theory_Data
@@ -153,7 +153,7 @@
   Graph.fold (fn (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm)
     (the_list assm_intro)) (Class_Data.get thy) [];
 
-fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
+fun these_defs thy = maps (Item_Net.content o #defs o the_class_data thy) o ancestry thy;
 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
 
 val base_morphism = #base_morph oo the_class_data;
@@ -226,7 +226,8 @@
     val add_class = Graph.new_node (class,
         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), ([], operations)))
+          Thm.trim_context of_class, Option.map Thm.trim_context some_axiom),
+          (Thm.item_net, operations)))
       #> fold (curry Graph.add_edge class) sups;
   in Class_Data.map add_class thy end;
 
@@ -261,7 +262,7 @@
   in
     thy
     |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apfst)
-        (cons sym_thm)
+        (Item_Net.update sym_thm)
     |> activate_defs class [sym_thm]
   end;
 
diff -r 46f66e821f5c -r 62b0577123a5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Aug 16 23:07:01 2021 +0200
@@ -668,33 +668,33 @@
 
 structure Thms = Generic_Data
 (
-  type T = thm list * thm list * thm list;
-  val empty = ([], [], []);
+  type T = thm Item_Net.T * thm Item_Net.T * thm Item_Net.T;
+  val empty = (Thm.item_net, Thm.item_net, Thm.item_net);
   val extend = I;
   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
-   (Thm.merge_thms (witnesses1, witnesses2),
-    Thm.merge_thms (intros1, intros2),
-    Thm.merge_thms (unfolds1, unfolds2));
+   (Item_Net.merge (witnesses1, witnesses2),
+    Item_Net.merge (intros1, intros2),
+    Item_Net.merge (unfolds1, unfolds2));
 );
 
 fun get_thms which ctxt =
   map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt)));
 
-val get_witnesses = get_thms #1;
-val get_intros = get_thms #2;
-val get_unfolds = get_thms #3;
+val get_witnesses = get_thms (Item_Net.content o #1);
+val get_intros = get_thms (Item_Net.content o #2);
+val get_unfolds = get_thms (Item_Net.content o #3);
 
 val witness_add =
   Thm.declaration_attribute (fn th =>
-    Thms.map (fn (x, y, z) => (Thm.add_thm (Thm.trim_context th) x, y, z)));
+    Thms.map (fn (x, y, z) => (Item_Net.update (Thm.trim_context th) x, y, z)));
 
 val intro_add =
   Thm.declaration_attribute (fn th =>
-    Thms.map (fn (x, y, z) => (x, Thm.add_thm (Thm.trim_context th) y, z)));
+    Thms.map (fn (x, y, z) => (x, Item_Net.update (Thm.trim_context th) y, z)));
 
 val unfold_add =
   Thm.declaration_attribute (fn th =>
-    Thms.map (fn (x, y, z) => (x, y, Thm.add_thm (Thm.trim_context th) z)));
+    Thms.map (fn (x, y, z) => (x, y, Item_Net.update (Thm.trim_context th) z)));
 
 
 (* Tactics *)
diff -r 46f66e821f5c -r 62b0577123a5 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Tools/named_thms.ML	Mon Aug 16 23:07:01 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 46f66e821f5c -r 62b0577123a5 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Aug 16 23:07:01 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);