src/Pure/display.ML
changeset 4440 9ed4098074bc
parent 4270 957c887b89b5
child 4498 a088ec3e4f5e
     1.1 --- a/src/Pure/display.ML	Fri Dec 19 09:58:42 1997 +0100
     1.2 +++ b/src/Pure/display.ML	Fri Dec 19 10:13:47 1997 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
     1.5  
     1.6      val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
     1.7 -    val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
     1.8 +    val spaces' = sort_wrt fst spaces;
     1.9      val {classes, classrel, default, tycons, abbrs, arities} =
    1.10        Type.rep_tsig tsig;
    1.11      val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
    1.12 @@ -219,10 +219,8 @@
    1.13      | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
    1.14      | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
    1.15  
    1.16 -  fun less_idx ((x, i):indexname, (y, j):indexname) =
    1.17 -    x < y orelse x = y andalso i < j;
    1.18 -  fun sort_idxs l = map (apsnd (sort less_idx)) l;
    1.19 -  fun sort_cnsts l = map (apsnd (sort_wrt fst)) l;
    1.20 +  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    1.21 +  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    1.22  
    1.23  
    1.24    (* prepare atoms *)