# HG changeset patch
# User wenzelm
# Date 1439466952 -7200
# Node ID 6584c0f3f0e06424de0039dd0c389e86d691e2eb
# Parent  61a7f9bb9e6bc5d6dda70d8322f73742e2fe4dfb# Parent  0ccb5fb83c24ef774981d9af2210a266553d69d1
merged

diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Library/refute.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -1156,7 +1156,7 @@
       error "Term to be refuted contains schematic type variables"
 
     (* existential closure over schematic variables *)
-    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
+    val vars = sort_by (fst o fst) (Term.add_vars t [])
     (* Term.term *)
     val ex_closure = fold (fn ((x, i), T) => fn t' =>
       HOLogic.exists_const T $
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Aug 13 13:55:52 2015 +0200
@@ -4,7 +4,6 @@
 Various tests for the proof reconstruction module.
 
 NOTE
-  - Makes use of the PolyML structure.
   - looks for THF proofs in the path indicated by $THF_PROOFS
   - these proofs are generated using LEO-II with the following
     configuration choices: -po 1 -nux -nuc --expand_extuni
@@ -39,13 +38,7 @@
   tptp_max_term_size = 0
 ]]
 
-ML {*
-  if test_all @{context} then ()
-  else
-    (Options.default_put_bool @{system_option ML_exception_trace} true;
-     default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
-     PolyML.Compiler.maxInlineSize := 0)
-*}
+declare [[ML_exception_trace, ML_print_depth = 200]]
 
 
 section "Importing proofs"
@@ -88,7 +81,7 @@
          Pretty.str (
           if is_none (#source_inf_opt data) then ""
           else ("\n\tannotation: " ^
-           PolyML.makestring (the (#source_inf_opt data : TPTP_Proof.source_info option))))])
+           @{make_string} (the (#source_inf_opt data : TPTP_Proof.source_info option))))])
     ) (rev fms);
 
 (*FIXME hack for testing*)
@@ -132,7 +125,7 @@
 val step_range_tester_tracing =
   step_range_tester
    (fn x => tracing ("@step " ^ Int.toString x))
-   (fn e => tracing ("!!" ^ PolyML.makestring e))
+   (fn e => tracing ("!!" ^ @{make_string} e))
 *}
 
 ML {*
@@ -258,7 +251,7 @@
       val thms_to_traceprint =
         map (fn thm => fn st =>
               (*FIXME uses makestring*)
-              print_tac ctxt (PolyML.makestring thm) st)
+              print_tac ctxt (@{make_string} thm) st)
 
     in
       if verbose then
@@ -345,7 +338,7 @@
   |> hd
   |> map #1
   |> TPTP_Reconstruct_Library.enumerate 0
-  |> List.app (PolyML.makestring #> writeln)
+  |> List.app (@{make_string} #> writeln)
   *}
 
 ML {*
@@ -607,7 +600,7 @@
 interpret_leo2_inference (* auto_based_reconstruction_tac *) (* oracle_based_reconstruction_tac *) prob_name (the ctxt'))
       else NONE
 
-(* val _ = tracing ("tt=" ^ PolyML.makestring the_tactics) *)
+(* val _ = tracing ("tt=" ^ @{make_string} the_tactics) *)
 
     val skeleton =
       if is_some thy' then
@@ -644,9 +637,9 @@
       TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
        (test_partial_reconstruction thy
         #> light_output ? erase_inference_fmlas
-        #> PolyML.makestring (* FIXME *)
-        #> (fn s => report (Proof_Context.init_global thy) (PolyML.makestring file ^ " === " ^ s ^
-             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> PolyML.makestring))))
+        #> @{make_string} (* FIXME *)
+        #> (fn s => report (Proof_Context.init_global thy) (@{make_string} file ^ " === " ^ s ^
+             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string}))))
        file
     end
 *}
@@ -675,7 +668,7 @@
           (TPTP_Reconstruct.reconstruct ctxt (fn prob_name =>
             TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference prob_name (* oracle_based_reconstruction_tac *))) prob_name )
        |> (fn s => report ctxt (Path.print file ^ " === " ^ Bool.toString s ^
-             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> PolyML.makestring))))
+             " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string}))))
        prob_name
     end
 *}
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Aug 13 13:55:52 2015 +0200
@@ -2,9 +2,6 @@
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Unit tests for proof reconstruction module.
-
-NOTE
-  - Makes use of the PolyML structure.
 *)
 
 theory TPTP_Proof_Reconstruction_Test_Units
@@ -12,15 +9,8 @@
 begin
 
 declare [[ML_exception_trace, ML_print_depth = 200]]
-ML {*
-PolyML.Compiler.maxInlineSize := 0;
-(* FIXME doesn't work with Isabelle?
-   PolyML.Compiler.debug := true *)
-*}
 
-declare [[
-  tptp_trace_reconstruction = true
-]]
+declare [[tptp_trace_reconstruction = true]]
 
 lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
 apply (tactic {*canonicalise_qtfr_order @{context} 1*})
@@ -941,7 +931,7 @@
 fun biggest_hyp_first_tac i = fn st =>
   let
     val results = TERMFUN biggest_hypothesis (SOME i) st
-val _ = tracing ("result=" ^ PolyML.makestring results)
+val _ = tracing ("result=" ^ @{make_string} results)
   in
     if null results then no_tac st
     else
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -173,7 +173,7 @@
         ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
       |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
         @{prop False}
-      |> #1 |> sort_wrt (heading_sort_key o fst)
+      |> #1 |> sort_by (heading_sort_key o fst)
     val prelude = fst (split_last problem)
     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
     val infers =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -2386,7 +2386,7 @@
 
 fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
   let
-    val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
+    val syms = sym_decl_tab |> Symtab.dest |> sort_by fst
     val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts
     val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
   in mono_lines @ decl_lines end
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -1625,7 +1625,7 @@
             Pretty.quote (Syntax.pretty_term ctxt bd)]]);
   in
     Pretty.big_list "Registered bounded natural functors:"
-      (map pretty_bnf (sort_wrt fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
+      (map pretty_bnf (sort_by fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
     |> Pretty.writeln
   end;
 
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -625,7 +625,7 @@
               Pretty.commas (map pretty_term ctrs))];
       in (xname, prt) end;
   in
-    Pretty.big_list "case translations:" (map #2 (sort_wrt #1 (map pretty_data cases)))
+    Pretty.big_list "case translations:" (map #2 (sort_by #1 (map pretty_data cases)))
     |> Pretty.writeln
   end;
 
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -472,7 +472,7 @@
       |> sort (nice_term_ord o apply2 fst)
       |> (case T of
             Type (@{type_name set}, _) =>
-            sort_wrt (truth_const_sort_key o snd)
+            sort_by (truth_const_sort_key o snd)
             #> make_set maybe_opt T'
           | _ =>
             make_plain_fun maybe_opt T1 T2
@@ -998,7 +998,7 @@
       if show andalso not (null names) then
         Pretty.str (title ^ plural_s_for_list names ^ ":")
         :: map (Pretty.indent indent_size o pretty_for_assign)
-               (sort_wrt (original_name o nickname_of) names)
+               (sort_by (original_name o nickname_of) names)
       else
         []
     fun free_name_for_term keep_all (x as (s, T)) =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/SMT/z3_isar.ML
--- a/src/HOL/Tools/SMT/z3_isar.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -70,7 +70,7 @@
 
 val reorder_foralls =
   dest_alls
-  #>> sort_wrt fst
+  #>> sort_by fst
   #-> fold_rev (Logic.all o Free);
 
 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -296,7 +296,7 @@
          $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
          s' :: taken)
       end)
-    (Term.add_vars t [] |> sort_wrt (fst o fst))
+    (Term.add_vars t [] |> sort_by (fst o fst))
   |> fst
 
 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -359,7 +359,7 @@
       (case outcome of
         NONE =>
         let
-          val used_facts = sort_wrt fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
+          val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred_methss =
             (Metis_Method (NONE, NONE),
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -253,7 +253,7 @@
     in
       (case used_facts of
         SOME used_facts =>
-        {outcome = NONE, used_facts = sort_wrt fst used_facts, used_from = used_from,
+        {outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from,
          preferred_methss = preferred_methss, run_time = run_time, message = message}
       | NONE => result)
     end
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -192,7 +192,7 @@
     val used_facts =
       (case fact_ids of
         NONE => map fst used_from
-      | SOME ids => sort_wrt fst (map (fst o snd) ids))
+      | SOME ids => sort_by fst (map (fst o snd) ids))
     val outcome = Option.map failure_of_smt_failure outcome
 
     val (preferred_methss, message) =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -49,7 +49,7 @@
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
-  maximum_ml_stack stack_limit @
+  ML_Stack.limit stack_limit @
   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun fork (params: params) body =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/General/name_space.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -602,7 +602,7 @@
   fold (fn (name, x) =>
     (verbose orelse not (is_concealed space name)) ?
       cons ((name, extern ctxt space name), x)) entries []
-  |> Library.sort_wrt (#2 o #1);
+  |> sort_by (#2 o #1);
 
 fun markup_entries verbose ctxt space entries =
   extern_entries verbose ctxt space entries
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -673,7 +673,7 @@
     val Ts = map #2 xs;
     val extraTs =
       (subtract (op =) (fold Term.add_tfreesT Ts []) (Term.add_tfrees body []))
-      |> Library.sort_wrt #1 |> map TFree;
+      |> sort_by #1 |> map TFree;
     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
 
     val args = map Logic.mk_type extraTs @ map Free xs;
@@ -794,7 +794,7 @@
       if null extraTs then ()
       else warning ("Additional type variable(s) in locale specification " ^
           Binding.print binding ^ ": " ^
-          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
+          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_by #1 extraTs)));
 
     val predicate_binding =
       if Binding.is_empty raw_predicate_binding then binding
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -102,7 +102,7 @@
    (if Context_Position.is_visible ctxt then
       warning
         ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
-          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
           (if mx = NoSyn then ""
            else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
     else (); NoSyn);
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -86,7 +86,7 @@
 );
 
 val get_commands = Data.get;
-val dest_commands = get_commands #> Symtab.dest #> sort_wrt #1;
+val dest_commands = get_commands #> Symtab.dest #> sort_by #1;
 val lookup_commands = Symtab.lookup o get_commands;
 
 fun help thy pats =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -1323,7 +1323,7 @@
     if null local_facts then []
     else
       [Pretty.big_list "local facts:"
-        (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
+        (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   end;
 
 fun print_local_facts verbose ctxt =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -65,7 +65,7 @@
     val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
     val facts = Global_Theory.facts_of thy;
     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
-    val prts = map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss));
+    val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
   in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
 
 fun pretty_theorems verbose thy =
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ML-Systems/maximum_ml_stack_dummy.ML
--- a/src/Pure/ML-Systems/maximum_ml_stack_dummy.ML	Thu Aug 13 11:14:16 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      Pure/ML-Systems/maximum_ml_stack_dummy.ML
-
-Maximum stack size (in words) for ML threads -- dummy version.
-*)
-
-fun maximum_ml_stack (_: int option) : Thread.threadAttribute list = [];
-
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML	Thu Aug 13 11:14:16 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
-
-Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
-*)
-
-fun maximum_ml_stack limit = [Thread.MaximumMLStack limit];
-
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ML-Systems/ml_stack_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_stack_dummy.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_stack_dummy.ML
+
+Maximum stack size (in words) for ML threads -- dummy version.
+*)
+
+signature ML_STACK =
+sig
+  val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit (_: int option) : Thread.threadAttribute list = [];
+
+end;
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
+
+Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
+*)
+
+signature ML_STACK =
+sig
+  val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit m = [Thread.MaximumMLStack m];
+
+end;
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -61,8 +61,8 @@
 use "ML-Systems/multithreading_polyml.ML";
 
 if ML_System.name = "polyml-5.5.3"
-then use "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
-else use "ML-Systems/maximum_ml_stack_dummy.ML";
+then use "ML-Systems/ml_stack_polyml-5.5.3.ML"
+else use "ML-Systems/ml_stack_dummy.ML";
 
 use "ML-Systems/unsynchronized.ML";
 val _ = PolyML.Compiler.forgetValue "ref";
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -18,7 +18,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
-use "ML-Systems/maximum_ml_stack_dummy.ML";
+use "ML-Systems/ml_stack_dummy.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/ml_name_space.ML";
 structure PolyML = struct end;
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/ROOT	Thu Aug 13 13:55:52 2015 +0200
@@ -6,8 +6,6 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/maximum_ml_stack_dummy.ML"
-    "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_compiler_parameters.ML"
     "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
     "ML-Systems/ml_debugger.ML"
@@ -17,6 +15,8 @@
     "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
+    "ML-Systems/ml_stack_dummy.ML"
+    "ML-Systems/ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
@@ -41,8 +41,6 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/maximum_ml_stack_dummy.ML"
-    "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_compiler_parameters.ML"
     "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
     "ML-Systems/ml_debugger.ML"
@@ -52,6 +50,8 @@
     "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
+    "ML-Systems/ml_stack_dummy.ML"
+    "ML-Systems/ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -429,7 +429,7 @@
             map prod_of_chain (these (AList.lookup (op =) chains tag));
       in map (pretty_prod name) nt_prods end;
 
-  in maps pretty_nt (sort_wrt fst (Symtab.dest tags)) end;
+  in maps pretty_nt (sort_by fst (Symtab.dest tags)) end;
 
 
 
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -176,7 +176,7 @@
       Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
     fun print_all () =
       #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
-      |> sort_wrt #1 |> map (Pretty.item o single o print o #2)
+      |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   in Context.setmp_thread_data (SOME context) print_all () end;
 
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/display.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -135,7 +135,7 @@
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
       ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @
-        Pretty.commas (map prt_const' (sort_wrt #1 rhs)));
+        Pretty.commas (map prt_const' (sort_by #1 rhs)));
 
     fun pretty_restrict (const, name) =
       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
@@ -171,10 +171,10 @@
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
         (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
-      |> sort_wrt (#1 o #1)
+      |> sort_by (#1 o #1)
       |> List.partition (null o #2)
       ||> List.partition (Defs.plain_args o #2 o #1);
-    val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
+    val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.display_names thy)] @
     [Pretty.big_list "classes:" (map pretty_classrel clsses),
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/facts.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -201,7 +201,7 @@
     if exists (fn prev => defined prev name) prev_facts orelse
       not verbose andalso is_concealed facts name then I
     else cons (name, ths)) facts []
-  |> sort_wrt #1;
+  |> sort_by #1;
 
 
 (* indexed props *)
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/goal_display.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -58,7 +58,7 @@
     | _ => I);
 
 fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
-fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
+fun sort_cnsts cs = map (apsnd (sort_by fst)) cs;
 
 fun consts_of t = sort_cnsts (add_consts t []);
 fun vars_of t = sort_idxs (add_vars t []);
diff -r 61a7f9bb9e6b -r 6584c0f3f0e0 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Aug 13 11:14:16 2015 +0200
+++ b/src/Pure/library.ML	Thu Aug 13 13:55:52 2015 +0200
@@ -193,7 +193,7 @@
   val sort: ('a * 'a -> order) -> 'a list -> 'a list
   val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
   val sort_strings: string list -> string list
-  val sort_wrt: ('a -> string) -> 'a list -> 'a list
+  val sort_by: ('a -> string) -> 'a list -> 'a list
   val tag_list: int -> 'a list -> (int * 'a) list
   val untag_list: (int * 'a) list -> 'a list
   val order_list: (int * 'a) list -> 'a list
@@ -955,7 +955,7 @@
 fun sort_distinct ord = mergesort true ord;
 
 val sort_strings = sort string_ord;
-fun sort_wrt key xs = sort (string_ord o apply2 key) xs;
+fun sort_by key xs = sort (string_ord o apply2 key) xs;
 
 
 (* items tagged by integer index *)