src/Pure/Isar/context_rules.ML
changeset 16512 1fa048f2a590
parent 16424 18a07ad8fea8
child 17314 04e21a27c0ad
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Jun 21 09:35:31 2005 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Jun 21 09:35:32 2005 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4      fun prt_kind (i, b) =
     1.5        Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     1.6          (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
     1.7 -          (sort (Int.compare o pairself fst) rules));
     1.8 +          (sort (int_ord o pairself fst) rules));
     1.9    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.10  
    1.11  
    1.12 @@ -175,10 +175,10 @@
    1.13        else x :: untaglist rest;
    1.14  
    1.15  fun orderlist brls =
    1.16 -  untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    1.17 +  untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    1.18  
    1.19  fun orderlist_no_weight brls =
    1.20 -  untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    1.21 +  untaglist (sort (int_ord o pairself (snd o fst)) brls);
    1.22  
    1.23  fun may_unify weighted t net =
    1.24    map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));