# HG changeset patch
# User wenzelm
# Date 1120489631 -7200
# Node ID 6c038c13fd0ff2d553224b93665221d41f3bce00
# Parent  671bd433b9eb7c94a6c0772fa7000361e2396946
use fast_string_ord;

diff -r 671bd433b9eb -r 6c038c13fd0f src/Pure/net.ML
--- a/src/Pure/net.ML	Mon Jul 04 17:07:10 2005 +0200
+++ b/src/Pure/net.ML	Mon Jul 04 17:07:11 2005 +0200
@@ -96,11 +96,12 @@
         | ins1 (AtomK a :: keys, Net{comb,var,alist}) =
             let fun newpair net = (a, ins1(keys,net))
                 fun inslist [] = [newpair empty]
-                  | inslist((b: string, netb) :: alist) =
-                      if a=b then newpair netb :: alist
-                      else if a<b then (*absent, ins1ert in alist*)
+                  | inslist ((b, netb) :: alist) =
+                      (case fast_string_ord (a, b) of
+                        EQUAL => newpair netb :: alist
+                      | LESS => (*absent, insert in alist*)
                           newpair empty :: (b,netb) :: alist
-                      else (*a>b*) (b,netb) :: inslist alist
+                      | GREATER => (b,netb) :: inslist alist)
             in  Net{comb=comb, var=var, alist= inslist alist}  end
   in  ins1 (keys,net)  end;
 
@@ -133,25 +134,28 @@
         | del1 (AtomK a :: keys, Net{comb,var,alist}) =
             let fun newpair net = (a, del1(keys,net))
                 fun dellist [] = raise DELETE
-                  | dellist((b: string, netb) :: alist) =
-                      if a=b then conspair(newpair netb, alist)
-                      else if a<b then (*absent*) raise DELETE
-                      else (*a>b*)  (b,netb) :: dellist alist
+                  | dellist((b, netb) :: alist) =
+                      (case fast_string_ord (a, b) of
+                        EQUAL => conspair(newpair netb, alist)
+                      | LESS => (*absent*) raise DELETE
+                      | GREATER => (b,netb) :: dellist alist)
             in  newnet{comb=comb, var=var, alist= dellist alist}  end
   in  del1 (keys,net)  end;
 
 fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
 
+
 (*** Retrieval functions for discrimination nets ***)
 
 exception OASSOC;
 
 (*Ordered association list lookup*)
-fun oassoc ([], a: string) = raise OASSOC
+fun oassoc ([], a) = raise OASSOC
   | oassoc ((b,x)::pairs, a) =
-      if b<a then oassoc(pairs,a)
-      else if a=b then x
-      else raise OASSOC;
+      (case fast_string_ord (a, b) of
+        EQUAL => x
+      | LESS => raise OASSOC
+      | GREATER => oassoc(pairs,a));
 
 (*Return the list of items at the given node, [] if no such node*)
 fun lookup (Leaf(xs), []) = xs