Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.

--- a/src/Pure/General/heap.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/General/heap.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -56,7 +56,7 @@
   | merge (Empty, h) = h
   | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
       (case ord (x1, x2) of
-        Library.GREATER => heap x2 a2 (merge (h1, b2))
+        GREATER => heap x2 a2 (merge (h1, b2))
       | _ => heap x1 a1 (merge (b1, h2)));
 
 fun insert (x, h) = merge (Heap (1, x, Empty, Empty), h);

--- a/src/Pure/Isar/context_rules.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/Isar/context_rules.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -115,7 +115,7 @@
     fun prt_kind (i, b) =
       Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
         (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
-          (sort (int_ord o pairself fst) rules));
+          (sort (Int.compare o pairself fst) rules));
   in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 
 
@@ -175,8 +175,10 @@
       if k = k' then untaglist rest
       else x :: untaglist rest;
 
-fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
-fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
+fun orderlist brls = 
+    untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
+fun orderlist_no_weight brls = 
+    untaglist (sort (Int.compare o pairself (snd o fst)) brls);
 
 fun may_unify weighted t net =
   map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));

--- a/src/Pure/Isar/net_rules.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/Isar/net_rules.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -38,7 +38,8 @@
 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)));
+  Tactic.untaglist 
+     ((Library.sort (Int.compare o pairself #1) (Net.unify_term net tm)));
 
 
 (* build rules *)

--- a/src/Pure/Proof/extraction.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -110,7 +110,7 @@
           Pattern.unify (sign, env, [pairself rew p])) (env', prems')
       in Some (Envir.norm_term env'' (inc (ren tm2)))
       end handle Pattern.MATCH => None | Pattern.Unif => None)
-        (sort (int_ord o pairself fst)
+        (sort (Int.compare o pairself fst)
           (Net.match_term rules (Pattern.eta_contract tm)));
 
   in rew end;

--- a/src/Pure/display.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/display.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -287,7 +287,7 @@
   | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
 
-fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+fun sort_idxs vs = map (apsnd (sort (prod_ord String.compare Int.compare))) vs;
 fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
 
 fun consts_of t = sort_cnsts (add_consts (t, []));

--- a/src/Pure/library.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/library.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -228,7 +228,6 @@
   val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
 
   (*orders*)
-  datatype order = LESS | EQUAL | GREATER
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   val int_ord: int * int -> order
@@ -1073,8 +1072,6 @@
 
 (** orders **)
 
-datatype order = LESS | EQUAL | GREATER;
-
 fun rev_order LESS = GREATER
   | rev_order EQUAL = EQUAL
   | rev_order GREATER = LESS;
@@ -1085,11 +1082,13 @@
   else if rel (y, x) then GREATER
   else EQUAL;
 
+(*Better to use Int.compare*)
 fun int_ord (i, j: int) =
   if i < j then LESS
   else if i = j then EQUAL
   else GREATER;
 
+(*Better to use String.compare*)
 fun string_ord (a, b: string) =
   if a < b then LESS
   else if a = b then EQUAL

--- a/src/Pure/term.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/term.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -191,6 +191,7 @@
   val typs_ord: typ list * typ list -> order
   val term_ord: term * term -> order
   val terms_ord: term list * term list -> order
+  val hd_ord: term * term -> order
   val termless: term * term -> bool
   val dummy_patternN: string
   val no_dummy_patterns: term -> term
@@ -984,17 +985,17 @@
 (** type and term orders **)
 
 fun indexname_ord ((x, i), (y, j)) =
-  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
+  (case Int.compare (i, j) of EQUAL => String.compare (x, y) | ord => ord);
 
-val sort_ord = list_ord string_ord;
+val sort_ord = list_ord String.compare;
 
 
 (* typ_ord *)
 
-fun typ_ord (Type x, Type y) = prod_ord string_ord typs_ord (x, y)
+fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y)
   | typ_ord (Type _, _) = GREATER
   | typ_ord (TFree _, Type _) = LESS
-  | typ_ord (TFree x, TFree y) = prod_ord string_ord sort_ord (x, y)
+  | typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y)
   | typ_ord (TFree _, TVar _) = GREATER
   | typ_ord (TVar _, Type _) = LESS
   | typ_ord (TVar _, TFree _) = LESS
@@ -1019,14 +1020,14 @@
 fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
       (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   | term_ord (t, u) =
-      (case int_ord (size_of_term t, size_of_term u) of
+      (case Int.compare (size_of_term t, size_of_term u) of
         EQUAL =>
           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
             (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
           end
       | ord => ord)
 and hd_ord (f, g) =
-  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
+  prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g)
 and terms_ord (ts, us) = list_ord term_ord (ts, us);
 
 fun termless tu = (term_ord tu = LESS);