improved Net interface;

--- a/src/FOLP/simp.ML	Wed Jul 13 16:07:18 2005 +0200
+++ b/src/FOLP/simp.ML	Wed Jul 13 16:07:21 2005 +0200
@@ -68,7 +68,7 @@
 
 (*insert a thm in a discrimination net by its lhs*)
 fun lhs_insert_thm (th,net) =
-    Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)
+    Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
     handle  Net.INSERT => net;
 
 (*match subgoal i against possible theorems in the net.
@@ -247,7 +247,7 @@
 
 (*insert a thm in a thm net*)
 fun insert_thm_warn (th,net) = 
-  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
+  Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
   handle Net.INSERT => 
     (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
      net);
@@ -273,7 +273,7 @@
 
 (*delete a thm from a thm net*)
 fun delete_thm_warn (th,net) = 
-  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
+  Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
   handle Net.DELETE => 
     (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
      net);

--- a/src/HOL/Tools/res_axioms.ML	Wed Jul 13 16:07:18 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 13 16:07:21 2005 +0200
@@ -250,7 +250,7 @@
        |> ObjectLogic.atomize_thm |> make_nnf;
 
 (*The cache prevents repeated clausification of a theorem, 
-  and also repeated declaration of Skolem functions*)  
+  and also repeated declaration of Skolem functions*)  (* FIXME better use Termtab!? *)
 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
@@ -366,10 +366,8 @@
     end;
 
 fun simpset_rules_of_thy thy =
-    let val rules = #rules(fst (rep_ss (simpset_of thy)))
-    in
-	map (fn (_,r) => (#name r, #thm r)) (Net.dest rules)
-    end;
+    let val rules = #rules (fst (rep_ss (simpset_of thy)))
+    in map (fn r => (#name r, #thm r)) (Net.entries rules) end;
 
 
 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)

--- a/src/Pure/Isar/net_rules.ML	Wed Jul 13 16:07:18 2005 +0200
+++ b/src/Pure/Isar/net_rules.ML	Wed Jul 13 16:07:21 2005 +0200
@@ -47,7 +47,7 @@
 
 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));
+    (Net.insert_term (K false) (index rule, (next, rule)) net);
 
 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
   let val rules = Library.gen_merge_lists' eq rules1 rules2
@@ -56,7 +56,7 @@
 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 index (Library.gen_rem eq (rules, rule)) next
-    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
+    (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*)
 

--- a/src/Pure/Proof/extraction.ML	Wed Jul 13 16:07:18 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Jul 13 16:07:21 2005 +0200
@@ -79,8 +79,8 @@
 val empty_rules : rules = {next = 0, rs = [], net = Net.empty};
 
 fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
-  {next = next - 1, rs = r :: rs, net = Net.insert_term
-     ((Pattern.eta_contract lhs, (next, r)), net, K false)};
+  {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
+     (Pattern.eta_contract lhs, (next, r)) net};
 
 fun merge_rules
   ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
@@ -316,7 +316,7 @@
       ExtractionData.get thy;
     val procs = List.concat (map (fst o snd) types);
     val rtypes = map fst types;
-    val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
+    val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     val thy' = add_syntax thy;
     val rd = ProofSyntax.read_proof thy' false
   in fn (thm, (vs, s1, s2)) =>
@@ -351,7 +351,7 @@
     val {realizes_eqns, typeof_eqns, defs, types, ...} =
       ExtractionData.get thy';
     val procs = List.concat (map (fst o snd) types);
-    val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
+    val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
       (map (Logic.dest_equals o prop_of) defs) [] prop;
   in freeze_thaw (condrew thy' eqns
@@ -470,7 +470,7 @@
     val typroc = typeof_proc (Sign.defaultS thy');
     val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o
       Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
-    val rrews = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
+    val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
 
     fun find_inst prop Ts ts vs =
       let

--- a/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:18 2005 +0200
+++ b/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:21 2005 +0200
@@ -58,12 +58,12 @@
           cs)
   else
       TC{rules  = th::rules,
-         net = Net.insert_term ((concl_of th, th), net, K false)};
+         net = Net.insert_term (K false) (concl_of th, th) net};
 
 
 fun delTC (cs as TC{rules, net}, th) =
   if mem_thm (th, rules) then
-      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
+      TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net,
          rules  = rem_thm (rules,th)}
   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
         cs);
@@ -113,7 +113,7 @@
 
 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
     TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
-        net = Net.merge (net, net', Drule.eq_thm_prop)};
+        net = Net.merge Drule.eq_thm_prop (net, net')};
 
 (*print tcsets*)
 fun print_tc (TC{rules,...}) =