# HG changeset patch
# User wenzelm
# Date 1255616122 -7200
# Node ID 63db9da65a1976cac1a432d715132d5686672d10
# Parent  ecc0705174c251814d3605495e39911a04e4f0e0
sort_strings (cf. Pure/library.ML);

diff -r ecc0705174c2 -r 63db9da65a19 src/HOL/Import/proof_kernel.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') =
diff -r ecc0705174c2 -r 63db9da65a19 src/HOL/SMT/Tools/smt_solver.ML
--- 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 =