diff -r 3c1f302b3ee6 -r a513730db7b0 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
@@ -210,7 +210,7 @@
 
 (**** PARSING OF TSTP FORMAT ****)
 
-(*Strings enclosed in single quotes, e.g. filenames*)
+(* Strings enclosed in single quotes (e.g., file names) *)
 val scan_general_id =
   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
@@ -277,6 +277,7 @@
                  --| Scan.option ($$ "," |-- parse_annotations false)) []
 
 val vampire_unknown_fact = "unknown"
+val tofof_fact_prefix = "fof_"
 
 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\).
    The <num> could be an identifier, but we assume integers. *)
@@ -290,7 +291,10 @@
             val (name, deps) =
               case deps of
                 ["file", _, s] =>
-                ((num, if s = vampire_unknown_fact then NONE else SOME s), [])
+                ((num,
+                  if s = vampire_unknown_fact then NONE
+                  else SOME (s |> perhaps (try (unprefix tofof_fact_prefix)))),
+                 [])
               | _ => ((num, NONE), deps)
           in
             case role of