sort_distinct;
authorwenzelm
Sat Dec 17 01:00:40 2005 +0100 (2005-12-17)
changeset 184284059413acbc1
parent 18427 b7ee916ae3ec
child 18429 42ee9f24f63a
sort_distinct;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
src/Pure/sorts.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Dec 17 01:00:38 2005 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Dec 17 01:00:40 2005 +0100
     1.3 @@ -678,8 +678,8 @@
     1.4      val occs1 = type_occs_of ctxt1 and occs2 = type_occs_of ctxt2;
     1.5      val extras = Symtab.fold (fn (a, ts) =>
     1.6        if Symtab.defined occs1 a then I else fold (occs_free a) ts) occs2 [];
     1.7 -    val tfrees = map #1 extras |> Library.sort_strings |> Library.unique_strings;
     1.8 -    val frees = map #2 extras |> Library.sort_strings |> Library.unique_strings;
     1.9 +    val tfrees = map #1 extras |> sort_distinct string_ord;
    1.10 +    val frees = map #2 extras |> sort_distinct string_ord;
    1.11    in
    1.12      if null extras then ()
    1.13      else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^
     2.1 --- a/src/Pure/Syntax/syntax.ML	Sat Dec 17 01:00:38 2005 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Dec 17 01:00:40 2005 +0100
     2.3 @@ -278,7 +278,7 @@
     2.4      ({input = merge_lists' input1 input2,
     2.5        lexicon = Scan.merge_lexicons lexicon1 lexicon2,
     2.6        gram = Parser.merge_grams gram1 gram2,
     2.7 -      consts = unique_strings (sort_strings (consts1 @ consts2)),
     2.8 +      consts = sort_distinct string_ord (consts1 @ consts2),
     2.9        prmodes = merge_lists prmodes1 prmodes2,
    2.10        parse_ast_trtab =
    2.11          merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
     3.1 --- a/src/Pure/sorts.ML	Sat Dec 17 01:00:38 2005 +0100
     3.2 +++ b/src/Pure/sorts.ML	Sat Dec 17 01:00:40 2005 +0100
     3.3 @@ -140,7 +140,7 @@
     3.4  
     3.5  fun norm_sort _ [] = []
     3.6    | norm_sort _ (S as [_]) = S
     3.7 -  | norm_sort classes S = unique_strings (sort_strings (filter (minimal_class classes S) S));
     3.8 +  | norm_sort classes S = sort_distinct string_ord (filter (minimal_class classes S) S);
     3.9  
    3.10  
    3.11  (* certify *)