# HG changeset patch
# User blanchet
# Date 1304369535 -7200
# Node ID 9d774c5d42a25fa2f35ce26a64d624f9619f8faa
# Parent  a7a30721767ad4d3453505d29dc9b26fe397feb0
proper default for TPTP source filed

diff -r a7a30721767a -r 9d774c5d42a2 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon May 02 22:52:15 2011 +0200
@@ -111,6 +111,9 @@
   | string_for_symbol_type arg_tys res_ty =
     string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
 
+val default_source =
+  ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
+
 fun string_for_problem_line _ _ (Decl (ident, sym, arg_tys, res_ty)) =
     "tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     string_for_symbol_type arg_tys res_ty ^ ").\n"
@@ -130,7 +133,7 @@
          (NONE, NONE) => ""
        | (SOME tm, NONE) => ", " ^ string_for_term tm
        | (_, SOME tm) =>
-         ", " ^ string_for_term (source |> the_default (ATerm ("[]", []))) ^
+         ", " ^ string_for_term (source |> the_default default_source) ^
          ", " ^ string_for_term tm) ^ ").\n"
     end
 fun tptp_strings_for_atp_problem hypothesis_kind format problem =