# HG changeset patch
# User wenzelm
# Date 1007518683 -3600
# Node ID 389d11fb62c8e0c1c24456e020e92564c8672c25
# Parent  86e383f6bfea1d2af6af1a9c8b10bf5f84045f6e
removed unused functionality (weight etc.);

diff -r 86e383f6bfea -r 389d11fb62c8 src/Pure/Isar/net_rules.ML
--- a/src/Pure/Isar/net_rules.ML	Wed Dec 05 03:17:34 2001 +0100
+++ b/src/Pure/Isar/net_rules.ML	Wed Dec 05 03:18:03 2001 +0100
@@ -11,13 +11,10 @@
   type 'a T
   val rules: 'a T -> 'a list
   val retrieve: 'a T -> term -> 'a list
-  val retrieve_weighted: 'a T -> term -> 'a list
-  val init: ('a * 'a -> bool) -> ('a -> int) -> ('a -> term) -> 'a T
+  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 deletes: 'a list -> 'a T -> 'a T
-  val inserts: 'a list -> 'a T -> 'a T
   val intro: thm T
   val elim: thm T
 end;
@@ -30,57 +27,44 @@
 datatype 'a T =
   Rules of {
     eq: 'a * 'a -> bool,
-    weight: 'a -> int,
     index: 'a -> term,
     rules: 'a list,
     next: int,
-    net: ((int * int) * 'a) Net.net};
+    net: (int * 'a) Net.net};
 
-fun mk_rules eq weight index rules next net =
-  Rules {eq = eq, weight = weight, index = index, rules = rules, next = next, 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;
 
-
-(* retrieve rules *)
-
-fun gen_retrieve order (Rules {rules, net, ...}) tm =
-  Tactic.untaglist (map (fn ((_, k), x) => (k, x))
-    (sort (order o pairself #1) (Net.unify_term net tm)));
-
-fun retrieve x = gen_retrieve (int_ord o pairself snd) x;
-fun retrieve_weighted x = gen_retrieve (prod_ord int_ord int_ord) x;
+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 weight index = mk_rules eq weight index [] ~1 Net.empty;
+fun init eq index = mk_rules eq index [] ~1 Net.empty;
 
-fun add rule (Rules {eq, weight, index, rules, next, net}) =
-  mk_rules eq weight index (rule :: rules) (next - 1)
-    (Net.insert_term ((index rule, ((weight rule, next), rule)), net, K false));
-
-fun make eq weight index rules = foldr (uncurry add) (rules, init eq weight index);
-
+fun add rule (Rules {eq, index, rules, next, net}) =
+  mk_rules eq index (rule :: rules) (next - 1)
+    (Net.insert_term ((index rule, (next, rule)), net, K false));
 
-fun merge (Rules {eq, weight, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
-  make eq weight index (Library.gen_merge_lists' eq rules1 rules2);
+fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
+  let val rules = Library.gen_merge_lists' eq rules1 rules2
+  in foldr (uncurry add) (rules, init eq index) end;
 
-fun delete rule (rs as Rules {eq, weight, index, rules, next, net}) =
+fun delete rule (rs as Rules {eq, index, rules, next, net}) =
   if not (Library.gen_mem eq (rule, rules)) then rs
-  else mk_rules eq weight index (Library.gen_rem eq (rules, rule)) next
-    (Net.delete_term ((index rule, ((0, 0), rule)), net, eq o pairself #2));
+  else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
+    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
 
-fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
-
-fun deletes rules rs = foldr (uncurry delete) (rules, rs);
-fun inserts rules rs = foldr (uncurry insert) (rules, rs);
+fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
 
 
 (* intro/elim rules *)
 
-val intro = init Thm.eq_thm Thm.nprems_of Thm.concl_of;
-val elim = init Thm.eq_thm Thm.nprems_of Thm.major_prem_of;
+val intro = init Thm.eq_thm Thm.concl_of;
+val elim = init Thm.eq_thm Thm.major_prem_of;
 
 
 end;