# HG changeset patch
# User desharna
# Date 1632306309 -7200
# Node ID d8dbe7525ff1f1d9eac3921e26d7117cd4881fb2
# Parent  398b7bb9ebdd030c3ddc273eb92c2de106c6a294
enabled FOOL for Vampire in Sledgehammer

diff -r 398b7bb9ebdd -r d8dbe7525ff1 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 10:46:42 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 12:25:09 2021 +0200
@@ -488,7 +488,7 @@
 
 val vampire_config : atp_config =
   let
-    val format = TFF (Without_FOOL, Monomorphic)
+    val format = TFF (With_FOOL, Monomorphic)
   in
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>