1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Fri Feb 03 18:00:55 2012 +0100
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Feb 03 18:00:55 2012 +0100
     1.3 @@ -102,8 +102,8 @@
     1.4  fun inference infers ident =
     1.5    these (AList.lookup (op =) infers ident) |> inference_term
     1.6  fun add_inferences_to_problem_line infers
     1.7 -                                   (Formula (ident, Axiom, phi, NONE, NONE)) =
     1.8 -    Formula (ident, Lemma, phi, inference infers ident, NONE)
     1.9 +                                   (Formula (ident, Axiom, phi, NONE, tms)) =
    1.10 +    Formula (ident, Lemma, phi, inference infers ident, tms)
    1.11    | add_inferences_to_problem_line _ line = line
    1.12  fun add_inferences_to_problem infers =
    1.13    map (apsnd (map (add_inferences_to_problem_line infers)))
    1.14 @@ -139,7 +139,7 @@
    1.15      exists (fn prefix => String.isPrefix prefix ident)
    1.16             likely_tautology_prefixes andalso
    1.17      is_none (run_some_atp ctxt format
    1.18 -                 [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
    1.19 +                 [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
    1.20    | is_problem_line_tautology _ _ _ = false
    1.21  
    1.22  structure String_Graph = Graph(type key = string val ord = string_ord);