turned structure NetRules into general Item_Net, which is loaded earlier;

--- a/src/Pure/IsaMakefile	Tue Mar 17 14:09:20 2009 +0100
+++ b/src/Pure/IsaMakefile	Tue Mar 17 14:12:06 2009 +0100
@@ -61,7 +61,7 @@
   Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML			\
   Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML		\
   Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
-  Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML	\
+  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
   Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML		\
   Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML		\
   Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
@@ -89,12 +89,12 @@
   Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
   conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
   defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
-  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
-  morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
-  primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
-  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML	\
-  term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML		\
-  type_infer.ML unify.ML variable.ML
+  interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML	\
+  more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML	\
+  pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML	\
+  search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML		\
+  tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML		\
+  type.ML type_infer.ML unify.ML variable.ML
 	@./mk
 
 

--- a/src/Pure/Isar/ROOT.ML	Tue Mar 17 14:09:20 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML	Tue Mar 17 14:12:06 2009 +0100
@@ -44,7 +44,6 @@
 use "proof.ML";
 use "../ML/ml_thms.ML";
 use "element.ML";
-use "net_rules.ML";
 
 (*derived theory and proof elements*)
 use "calculation.ML";
@@ -89,5 +88,3 @@
 use "../Thy/thm_deps.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";
-
-

--- a/src/Pure/Isar/net_rules.ML	Tue Mar 17 14:09:20 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Pure/Isar/net_rules.ML
-    Author:     Markus Wenzel, TU Muenchen
-
-Efficient storage of rules: preserves order, prefers later entries.
-*)
-
-signature NET_RULES =
-sig
-  type 'a T
-  val rules: 'a T -> 'a list
-  val retrieve: 'a T -> term -> 'a list
-  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
-  val merge: 'a T * 'a T -> 'a T
-  val delete: 'a -> 'a T -> 'a T
-  val insert: 'a -> 'a T -> 'a T
-  val intro: thm T
-  val elim: thm T
-end;
-
-structure NetRules: NET_RULES =
-struct
-
-(* datatype rules *)
-
-datatype 'a T =
-  Rules of {
-    eq: 'a * 'a -> bool,
-    index: 'a -> term,
-    rules: 'a list,
-    next: int,
-    net: (int * 'a) Net.net};
-
-fun mk_rules eq index rules next net =
-  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
-
-fun rules (Rules {rules = rs, ...}) = rs;
-
-fun retrieve (Rules {rules, net, ...}) tm =
-  Tactic.untaglist 
-     ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
-
-
-(* build rules *)
-
-fun init eq index = mk_rules eq index [] ~1 Net.empty;
-
-fun add rule (Rules {eq, index, rules, next, net}) =
-  mk_rules eq index (rule :: rules) (next - 1)
-    (Net.insert_term (K false) (index rule, (next, rule)) net);
-
-fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
-  let val rules = Library.merge eq (rules1, rules2)
-  in fold_rev add rules (init eq index) end;
-
-fun delete rule (rs as Rules {eq, index, rules, next, net}) =
-  if not (member eq rules rule) then rs
-  else mk_rules eq index (remove eq rule rules) next
-    (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
-
-fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
-
-
-(* intro/elim rules *)
-
-val intro = init Thm.eq_thm_prop Thm.concl_of;
-val elim = init Thm.eq_thm_prop Thm.major_prem_of;
-
-
-end;

--- a/src/Pure/ROOT.ML	Tue Mar 17 14:09:20 2009 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 17 14:12:06 2009 +0100
@@ -52,11 +52,12 @@
 use "ML/ml_syntax.ML";
 
 (*core of tactical proof system*)
+use "net.ML";
+use "item_net.ML";
 use "envir.ML";
 use "consts.ML";
 use "primitive_defs.ML";
 use "defs.ML";
-use "net.ML";
 use "sign.ML";
 use "pattern.ML";
 use "unify.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/item_net.ML	Tue Mar 17 14:12:06 2009 +0100
@@ -0,0 +1,58 @@
+(*  Title:      Pure/item_net.ML
+    Author:     Markus Wenzel, TU Muenchen
+
+Efficient storage of items indexed by terms; preserves order and
+prefers later entries.
+*)
+
+signature ITEM_NET =
+sig
+  type 'a T
+  val content: 'a T -> 'a list
+  val retrieve: 'a T -> term -> 'a list
+  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
+  val merge: 'a T * 'a T -> 'a T
+  val delete: 'a -> 'a T -> 'a T
+  val insert: 'a -> 'a T -> 'a T
+end;
+
+structure Item_Net: ITEM_NET =
+struct
+
+(* datatype *)
+
+datatype 'a T =
+  Items of {
+    eq: 'a * 'a -> bool,
+    index: 'a -> term,
+    content: 'a list,
+    next: int,
+    net: (int * 'a) Net.net};
+
+fun mk_items eq index content next net =
+  Items {eq = eq, index = index, content = content, next = next, net = net};
+
+fun content (Items {content, ...}) = content;
+fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
+
+
+(* build net *)
+
+fun init eq index = mk_items eq index [] ~1 Net.empty;
+
+fun add x (Items {eq, index, content, next, net}) =
+  mk_items eq index (x :: content) (next - 1)
+    (Net.insert_term (K false) (index x, (next, x)) net);
+
+fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) =
+  let val content = Library.merge eq (content1, content2)
+  in fold_rev add content (init eq index) end;
+
+fun delete x (items as Items {eq, index, content, next, net}) =
+  if not (member eq content x) then items
+  else mk_items eq index (remove eq x content) next
+    (Net.delete_term (eq o pairself #2) (index x, (0, x)) net);
+
+fun insert x items = add x (delete x items);   (*ensure that added entry gets precedence*)
+
+end;