# HG changeset patch # User wenzelm # Date 1134777640 -3600 # Node ID 4059413acbc102c632b2825141df7eec7242eef4 # Parent b7ee916ae3ec5cb0f370e6be3ebef6a29f56ea85 sort_distinct; diff -r b7ee916ae3ec -r 4059413acbc1 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Dec 17 01:00:38 2005 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Dec 17 01:00:40 2005 +0100 @@ -678,8 +678,8 @@ val occs1 = type_occs_of ctxt1 and occs2 = type_occs_of ctxt2; val extras = Symtab.fold (fn (a, ts) => if Symtab.defined occs1 a then I else fold (occs_free a) ts) occs2 []; - val tfrees = map #1 extras |> Library.sort_strings |> Library.unique_strings; - val frees = map #2 extras |> Library.sort_strings |> Library.unique_strings; + val tfrees = map #1 extras |> sort_distinct string_ord; + val frees = map #2 extras |> sort_distinct string_ord; in if null extras then () else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ diff -r b7ee916ae3ec -r 4059413acbc1 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat Dec 17 01:00:38 2005 +0100 +++ b/src/Pure/Syntax/syntax.ML Sat Dec 17 01:00:40 2005 +0100 @@ -278,7 +278,7 @@ ({input = merge_lists' input1 input2, lexicon = Scan.merge_lexicons lexicon1 lexicon2, gram = Parser.merge_grams gram1 gram2, - consts = unique_strings (sort_strings (consts1 @ consts2)), + consts = sort_distinct string_ord (consts1 @ consts2), prmodes = merge_lists prmodes1 prmodes2, parse_ast_trtab = merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2, diff -r b7ee916ae3ec -r 4059413acbc1 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sat Dec 17 01:00:38 2005 +0100 +++ b/src/Pure/sorts.ML Sat Dec 17 01:00:40 2005 +0100 @@ -140,7 +140,7 @@ fun norm_sort _ [] = [] | norm_sort _ (S as [_]) = S - | norm_sort classes S = unique_strings (sort_strings (filter (minimal_class classes S) S)); + | norm_sort classes S = sort_distinct string_ord (filter (minimal_class classes S) S); (* certify *)