tuned;

--- a/src/Pure/General/scan.ML	Tue Jun 21 09:35:31 2005 +0200
+++ b/src/Pure/General/scan.ML	Tue Jun 21 09:35:32 2005 +0200
@@ -331,7 +331,7 @@
         fun ext (lex, chrs) =
           let
             fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
-                  (case String.compare (c, d) of
+                  (case string_ord (c, d) of
                     LESS => Branch (d, a, add lt chs, eq, gt)
                   | EQUAL => Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
                   | GREATER => Branch (d, a, lt, eq, add gt chs))
@@ -361,7 +361,7 @@
 fun is_literal Empty _ = false
   | is_literal _ [] = false
   | is_literal (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
-      (case String.compare (c, d) of
+      (case string_ord (c, d) of
         LESS => is_literal lt chs
       | EQUAL => a <> no_literal andalso null cs orelse is_literal eq cs
       | GREATER => is_literal gt chs);
@@ -374,7 +374,7 @@
     fun lit Empty res _ = res
       | lit (Branch _) _ [] = raise MORE NONE
       | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
-          (case String.compare (c, d) of
+          (case string_ord (c, d) of
             LESS => lit lt res chs
           | EQUAL => lit eq (if a = no_literal then res else SOME (a, cs)) cs
           | GREATER => lit gt res chs);

--- a/src/Pure/Isar/context_rules.ML	Tue Jun 21 09:35:31 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue Jun 21 09:35:32 2005 +0200
@@ -113,7 +113,7 @@
     fun prt_kind (i, b) =
       Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
         (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
-          (sort (Int.compare o pairself fst) rules));
+          (sort (int_ord o pairself fst) rules));
   in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 
 
@@ -175,10 +175,10 @@
       else x :: untaglist rest;
 
 fun orderlist brls =
-  untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
+  untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
 
 fun orderlist_no_weight brls =
-  untaglist (sort (Int.compare o pairself (snd o fst)) brls);
+  untaglist (sort (int_ord 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	Tue Jun 21 09:35:31 2005 +0200
+++ b/src/Pure/Isar/net_rules.ML	Tue Jun 21 09:35:32 2005 +0200
@@ -38,7 +38,7 @@
 
 fun retrieve (Rules {rules, net, ...}) tm =
   Tactic.untaglist 
-     ((Library.sort (Int.compare o pairself #1) (Net.unify_term net tm)));
+     ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
 
 
 (* build rules *)