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 43473 fb2713b803e6
parent 43465 5ca37e764139
child 43481 51857e7fa64b 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 20 09:19:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -49,8 +49,8 @@
   val extract_known_failure :
     (failure * string) list -> string -> failure option
   val extract_tstplike_proof_and_outcome :
-    bool -> bool -> int -> (string * string) list -> (failure * string) list
-    -> string -> string * failure option
+    bool -> bool -> (string * string) list -> (failure * string) list -> string
+    -> string * failure option
   val is_same_atp_step : step_name -> step_name -> bool
   val scan_general_id : string list -> string * string list
   val parse_formula :
@@ -194,7 +194,7 @@
   |> find_first (fn (_, pattern) => String.isSubstring pattern output)
   |> Option.map fst
 
-fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
+fun extract_tstplike_proof_and_outcome verbose complete proof_delims
                                        known_failures output =
   case (extract_tstplike_proof proof_delims output,
         extract_known_failure known_failures output) of
isabelle