src/Pure/Isar/context_rules.ML

--- 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));