--- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:42 2011 +0200
@@ -419,8 +419,9 @@
[TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
- [("#START OF PROOF", "Proved Goals:")] [] Hypothesis Hypothesis
- [CNF_UEQ] (K (500, ["poly_args"]) (* FUDGE *))
+ [("#START OF PROOF", "Proved Goals:")]
+ [(OutOfResources, "Too many function symbols")] Hypothesis
+ Hypothesis [CNF_UEQ] (K (100, ["poly_args"]) (* FUDGE *))
(* Setup *)