--- 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 " ^
--- 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,
--- 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 *)