# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID e58bcea9492a59bbc4684eb8c42634f762c4419d
# Parent  5b02f7757a4c5b503ffbcab67c64fbeaa0ad33a4
tuned ML

diff -r 5b02f7757a4c -r e58bcea9492a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -1029,8 +1029,7 @@
 fun raw_mangled_const_name type_name ty_args (s, s') =
   let
     fun type_suffix f g =
-      fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
-               ty_args ""
+      fold_rev (prefix o g o prefix mangled_type_sep o type_name f) ty_args ""
   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
 fun mangled_const_name type_enc =
   map_filter (atp_type_of_type_arg type_enc)
diff -r 5b02f7757a4c -r e58bcea9492a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -2136,7 +2136,7 @@
         val G = Int_Graph.make (map (apfst (rpair ())) deps);
         val sccs = map (sort int_ord) (Int_Graph.strong_conn G);
 
-        val str_of_scc = curry (op ^) (co_prefix fp ^ "datatype ") o
+        val str_of_scc = prefix (co_prefix fp ^ "datatype ") o
           space_implode " and " o map (suffix " = \<dots>" o Long_Name.base_name);
 
         fun warn [_] = ()
diff -r 5b02f7757a4c -r e58bcea9492a src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -135,7 +135,7 @@
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
-      |> curry (op ^) ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
+      |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
         " proof (of " ^ string_of_int (length facts) ^ "): ")
       |> writeln