diff -r c00febb8e39c -r 264881a20f50 src/HOL/Tools/ATP/atp_problem.ML
--- 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\