diff -r 733b7a3277b2 -r c9e8ad426ab1 src/HOL/Tools/ATP/atp_problem.ML
--- 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 =