--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 06 17:19:34 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 06 17:19:34 2011 +0100
@@ -273,8 +273,10 @@
|> enclose "(" ")"
| string_for_formula format (AAtom tm) = string_for_term format tm
-val default_source =
- ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
+fun the_source (SOME source) = source
+ | the_source NONE =
+ ATerm ("inference",
+ ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
fun string_for_format CNF = tptp_cnf
| string_for_format CNF_UEQ = tptp_cnf
@@ -292,7 +294,7 @@
(NONE, NONE) => ""
| (SOME tm, NONE) => ", " ^ string_for_term format tm
| (_, SOME tm) =>
- ", " ^ string_for_term format (source |> the_default default_source) ^
+ ", " ^ string_for_term format (the_source source) ^
", " ^ string_for_term format tm) ^ ").\n"
fun tptp_lines_for_atp_problem format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\