# HG changeset patch
# User blanchet
# Date 1406220398 -7200
# Node ID 49077e289606afe2f7acc27d9cb7d4edca7040e5
# Parent  dde0e76996adc6724a044f50ffc6c57e6e38ee97
filter out 'theory(...)' from dependencies early on

diff -r dde0e76996ad -r 49077e289606 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 24 18:46:38 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 24 18:46:38 2014 +0200
@@ -302,7 +302,8 @@
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x
 and parse_dependencies x =
-  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency) >> flat) x
+  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency)
+   >> (flat #> filter_out (curry (op =) "theory"))) x
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    -- Scan.option ($$ "," |-- scan_general_id
@@ -676,7 +677,7 @@
     _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
   | _ => NONE)
 
-fun atp_proof_of_tstplike_proof local_prover _ "" = []
+fun atp_proof_of_tstplike_proof _ _ "" = []
   | atp_proof_of_tstplike_proof local_prover problem tstp =
     (case core_of_agsyhol_proof tstp of
       SOME facts => facts |> map (core_inference agsyhol_core_rule)