tuned;
authorwenzelm
Tue Jun 21 09:35:32 2005 +0200 (2005-06-21)
changeset 165121fa048f2a590
parent 16511 dad516b121cd
child 16513 f38693aad717
tuned;
src/Pure/General/scan.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/net_rules.ML
     1.1 --- a/src/Pure/General/scan.ML	Tue Jun 21 09:35:31 2005 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Tue Jun 21 09:35:32 2005 +0200
     1.3 @@ -331,7 +331,7 @@
     1.4          fun ext (lex, chrs) =
     1.5            let
     1.6              fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
     1.7 -                  (case String.compare (c, d) of
     1.8 +                  (case string_ord (c, d) of
     1.9                      LESS => Branch (d, a, add lt chs, eq, gt)
    1.10                    | EQUAL => Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
    1.11                    | GREATER => Branch (d, a, lt, eq, add gt chs))
    1.12 @@ -361,7 +361,7 @@
    1.13  fun is_literal Empty _ = false
    1.14    | is_literal _ [] = false
    1.15    | is_literal (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
    1.16 -      (case String.compare (c, d) of
    1.17 +      (case string_ord (c, d) of
    1.18          LESS => is_literal lt chs
    1.19        | EQUAL => a <> no_literal andalso null cs orelse is_literal eq cs
    1.20        | GREATER => is_literal gt chs);
    1.21 @@ -374,7 +374,7 @@
    1.22      fun lit Empty res _ = res
    1.23        | lit (Branch _) _ [] = raise MORE NONE
    1.24        | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
    1.25 -          (case String.compare (c, d) of
    1.26 +          (case string_ord (c, d) of
    1.27              LESS => lit lt res chs
    1.28            | EQUAL => lit eq (if a = no_literal then res else SOME (a, cs)) cs
    1.29            | GREATER => lit gt res chs);
     2.1 --- a/src/Pure/Isar/context_rules.ML	Tue Jun 21 09:35:31 2005 +0200
     2.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Jun 21 09:35:32 2005 +0200
     2.3 @@ -113,7 +113,7 @@
     2.4      fun prt_kind (i, b) =
     2.5        Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     2.6          (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
     2.7 -          (sort (Int.compare o pairself fst) rules));
     2.8 +          (sort (int_ord o pairself fst) rules));
     2.9    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    2.10  
    2.11  
    2.12 @@ -175,10 +175,10 @@
    2.13        else x :: untaglist rest;
    2.14  
    2.15  fun orderlist brls =
    2.16 -  untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    2.17 +  untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
    2.18  
    2.19  fun orderlist_no_weight brls =
    2.20 -  untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    2.21 +  untaglist (sort (int_ord o pairself (snd o fst)) brls);
    2.22  
    2.23  fun may_unify weighted t net =
    2.24    map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
     3.1 --- a/src/Pure/Isar/net_rules.ML	Tue Jun 21 09:35:31 2005 +0200
     3.2 +++ b/src/Pure/Isar/net_rules.ML	Tue Jun 21 09:35:32 2005 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  
     3.5  fun retrieve (Rules {rules, net, ...}) tm =
     3.6    Tactic.untaglist 
     3.7 -     ((Library.sort (Int.compare o pairself #1) (Net.unify_term net tm)));
     3.8 +     ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
     3.9  
    3.10  
    3.11  (* build rules *)