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)