# HG changeset patch
# User blanchet
# Date 1402940461 -7200
# Node ID cab38f7a3adb2ba4b714a0eeea7ed4c14fc0baa3
# Parent  13db1d0787431a47ec9582b9ce17846b70751d51
use right delimiters for Waldmeister proofs

diff -r 13db1d078743 -r cab38f7a3adb src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Jun 16 19:41:00 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Jun 16 19:41:01 2014 +0200
@@ -34,7 +34,7 @@
 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
 
 lemma "1 + 1 = (2::nat)"
-sledgehammer [vampire, max_facts = 3]
+sledgehammer [remote_waldmeister, max_facts = 3, verbose, overlord]
 oops
 
 end
diff -r 13db1d078743 -r cab38f7a3adb src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 19:41:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 16 19:41:01 2014 +0200
@@ -718,11 +718,11 @@
    remotify_config system_name system_versions best_slice o config)
 
 fun gen_remote_waldmeister name =
-  remote_atp name "Waldmeister" ["710"]
-    [("#START OF PROOF", "Proved Goals:")]
-    [(OutOfResources, "Too many function symbols"),
-     (Inappropriate, "****  Unexpected end of file."),
-     (Crashed, "Unrecoverable Segmentation Fault")]
+  remote_atp name "Waldmeister" ["710"] tstp_proof_delims
+    ([(OutOfResources, "Too many function symbols"),
+      (Inappropriate, "****  Unexpected end of file."),
+      (Crashed, "Unrecoverable Segmentation Fault")]
+     @ known_szs_status_failures)
     Hypothesis
     (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))