src/Pure/Isar/proof_context.ML
changeset 18428 4059413acbc1
parent 18418 bf448d999b7e
child 18476 49dde7b7b14a
     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 " ^