1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 24 18:46:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 24 18:46:38 2014 +0200
     1.3 @@ -302,7 +302,8 @@
     1.4    (parse_inference_source >> snd
     1.5     || scan_general_id --| skip_term >> single) x
     1.6  and parse_dependencies x =
     1.7 -  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency) >> flat) x
     1.8 +  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency)
     1.9 +   >> (flat #> filter_out (curry (op =) "theory"))) x
    1.10  and parse_file_source x =
    1.11    (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    1.12     -- Scan.option ($$ "," |-- scan_general_id
    1.13 @@ -676,7 +677,7 @@
    1.14      _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
    1.15    | _ => NONE)
    1.16  
    1.17 -fun atp_proof_of_tstplike_proof local_prover _ "" = []
    1.18 +fun atp_proof_of_tstplike_proof _ _ "" = []
    1.19    | atp_proof_of_tstplike_proof local_prover problem tstp =
    1.20      (case core_of_agsyhol_proof tstp of
    1.21        SOME facts => facts |> map (core_inference agsyhol_core_rule)