--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 19:41:42 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 19:42:44 2014 +0200
@@ -155,7 +155,6 @@
open ATP_Util
-
val parens = enclose "(" ")"
(** ATP problem **)
@@ -385,8 +384,7 @@
val dfg_individual_type = "iii" (* cannot clash *)
-val suffix_type_of_types =
- suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
+val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
fun str_of_type format ty =
let
@@ -439,9 +437,7 @@
let
val of_type = string_of_type format
val of_term = tptp_string_of_term format
- fun app () =
- tptp_string_of_app format s
- (map of_type tys @ map of_term ts)
+ fun app () = tptp_string_of_app format s (map of_type tys @ map of_term ts)
in
if s = tptp_empty_list then
(* used for lists in the optional "source" field of a derivation *)