Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
filter out 'theory(...)' from dependencies early on
authorblanchet
Thu, 24 Jul 2014 18:46:38 +0200
changeset 57656 49077e289606
parent 57655 dde0e76996ad
child 57657 6840b23da81d
filter out 'theory(...)' from dependencies early on
src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle