src/Pure/Isar/context_rules.ML
changeset 14472 cba7c0a3ffb3
parent 13372 18790d503fe0
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Isar/context_rules.ML	Wed Mar 17 14:00:45 2004 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Mar 19 10:42:38 2004 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4      fun prt_kind (i, b) =
     1.5        Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     1.6          (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
     1.7 -          (sort (int_ord o pairself fst) rules));
     1.8 +          (sort (Int.compare o pairself fst) rules));
     1.9    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.10  
    1.11  
    1.12 @@ -175,8 +175,10 @@
    1.13        if k = k' then untaglist rest
    1.14        else x :: untaglist rest;
    1.15  
    1.16 -fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    1.17 -fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
    1.18 +fun orderlist brls = 
    1.19 +    untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    1.20 +fun orderlist_no_weight brls = 
    1.21 +    untaglist (sort (Int.compare 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));