# HG changeset patch
# User wenzelm
# Date 1439456719 -7200
# Node ID 610794dff23c647254545aabccc9e715a585f53c
# Parent  020becec359c0adaf49b2f616d0851a6dfd6d036
tuned signature, in accordance to sortBy in Scala;

diff -r 020becec359c -r 610794dff23c src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Library/refute.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -1623,7 +1623,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 020becec359c -r 610794dff23c src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/SMT/z3_isar.ML
--- a/src/HOL/Tools/SMT/z3_isar.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/General/name_space.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/display.ML
--- a/src/Pure/display.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/display.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/facts.ML
--- a/src/Pure/facts.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/facts.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/goal_display.ML	Thu Aug 13 11:05:19 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 020becec359c -r 610794dff23c src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/library.ML	Thu Aug 13 11:05:19 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 *)