--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Oct 06 19:19:16 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Oct 06 19:19:16 2014 +0200
@@ -96,6 +96,7 @@
val tptp_true : string
val tptp_lambda : string
val tptp_empty_list : string
+ val dfg_individual_type : string
val isabelle_info_prefix : string
val isabelle_info : string -> int -> (string, 'a) atp_term list
val extract_isabelle_status : (string, 'a) atp_term list -> string option
@@ -251,6 +252,9 @@
val tptp_true = "$true"
val tptp_lambda = "^"
val tptp_empty_list = "[]"
+
+val dfg_individual_type = "iii" (* cannot clash *)
+
val isabelle_info_prefix = "isabelle_"
val inductionN = "induction"
@@ -386,8 +390,6 @@
| uncurry_type _ =
raise Fail "unexpected higher-order type in first-order format"
-val dfg_individual_type = "iii" (* cannot clash *)
-
val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
fun str_of_type format ty =