sort_strings (cf. Pure/library.ML);
--- a/src/HOL/Import/proof_kernel.ML Thu Oct 15 15:53:33 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu Oct 15 16:15:22 2009 +0200
@@ -2177,7 +2177,7 @@
_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
- val tnames = sort string_ord (map fst tfrees)
+ val tnames = sort_strings (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
val ((_, typedef_info), thy') =
--- a/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 15 15:53:33 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 15 16:15:22 2009 +0200
@@ -226,7 +226,7 @@
fun print_setup gen =
let
val t = string_of_int (Config.get_generic gen timeout)
- val names = sort string_ord (all_solver_names_of (Context.theory_of gen))
+ val names = sort_strings (all_solver_names_of (Context.theory_of gen))
val ns = if null names then [no_solver] else names
val take_info = (fn (_, []) => NONE | info => SOME info)
val infos =