--- 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 $
--- 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
*}
--- 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
--- 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 =
--- 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
--- 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;
--- 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;
--- 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)) =
--- 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
--- 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
--- 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),
--- 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
--- 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) =
--- 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 =
--- 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
--- 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
--- 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);
--- 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 =
--- 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 =
--- 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 =
--- 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 = [];
-
--- 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];
-
--- /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;
--- /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;
--- 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";
--- 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;
--- 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"
--- 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;
--- 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;
--- 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),
--- 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 *)
--- 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 []);
--- 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 *)