# HG changeset patch
# User wenzelm
# Date 1257105314 -3600
# Node ID d74dc1b549308f5f0bb0cd0c447a43cbd573e3d6
# Parent  69531a7b55b694a6719365de1b521b9669118ffc
added insert_safe, delete_safe variants;

diff -r 69531a7b55b6 -r d74dc1b54930 src/Pure/net.ML
--- a/src/Pure/net.ML	Sun Nov 01 16:23:31 2009 +0100
+++ b/src/Pure/net.ML	Sun Nov 01 20:55:14 2009 +0100
@@ -22,9 +22,13 @@
   exception INSERT
   val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
   val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
+  val insert_safe: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
+  val insert_term_safe: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
   exception DELETE
   val delete: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net
   val delete_term: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net
+  val delete_safe: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net
+  val delete_term_safe: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net
   val lookup: 'a net -> key list -> 'a list
   val match_term: 'a net -> term -> 'a list
   val unify_term: 'a net -> term -> 'a list
@@ -99,8 +103,10 @@
             in  Net{comb=comb, var=var, atoms=atoms'}  end
   in  ins1 (keys,net)  end;
 
+fun insert_term eq (t, x) = insert eq (key_of_term t, x);
+
 fun insert_safe eq entry net = insert eq entry net handle INSERT => net;
-fun insert_term eq (t, x) = insert eq (key_of_term t, x);
+fun insert_term_safe eq entry net = insert_term eq entry net handle INSERT => net;
 
 
 (*** Deletion from a discrimination net ***)
@@ -137,6 +143,9 @@
 
 fun delete_term eq (t, x) = delete eq (key_of_term t, x);
 
+fun delete_safe eq entry net = delete eq entry net handle DELETE => net;
+fun delete_term_safe eq entry net = delete_term eq entry net handle DELETE => net;
+
 
 (*** Retrieval functions for discrimination nets ***)