# HG changeset patch
# User blanchet
# Date 1336637260 -7200
# Node ID 6213900d6d5f5a106f3a6be5a16b7985980f07ef
# Parent  9d978604aee4bde0a700d8cfa736dc7f27c307f7
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)

diff -r 9d978604aee4 -r 6213900d6d5f src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 09 11:24:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 10 10:07:40 2012 +0200
@@ -641,7 +641,7 @@
        (Inappropriate, "****  Unexpected end of file."),
        (Crashed, "Unrecoverable Segmentation Fault")]
       Hypothesis Hypothesis
-      (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))
+      (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
 
 (* Setup *)