Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_proof.ML
changeset 54836 47857a79bdad
parent 54820 d9ab86c044fd
child 55192 b75b52c7cf94 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 20 11:34:07 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 20 14:27:07 2013 +0100
@@ -465,7 +465,7 @@
   ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
      --| $$ ")") x
 fun parse_spass_pirate_inference_source x =
-  (scan_general_id |-- $$ "(" -- parse_spass_pirate_dependencies --| $$ ")") x
+  (scan_general_id -- ($$ "(" |-- parse_spass_pirate_dependencies --| $$ ")")) x
 fun parse_spass_pirate_source x =
   (parse_spass_pirate_file_source >> (fn s => File_Source ("", SOME s))
    || parse_spass_pirate_inference_source >> Inference_Source) x
isabelle