--- 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)
--- 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 [_] = ()
--- 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