# HG changeset patch
# User blanchet
# Date 1314103459 -7200
# Node ID 800baa1b1406ae6ef76fb7cf7b0eaffe124c9a5a
# Parent  c76c04d876ef0607ecdc9455c5f1742c5dd32b2b
fixed TFF slicing

diff -r c76c04d876ef -r 800baa1b1406 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -449,8 +449,7 @@
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
                (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["1.8"]
-               (K (200, TFF, "mangled_guards?") (* FUDGE *))
+  remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
 val remote_z3_atp =
   remotify_atp z3_atp "Z3" ["2.18"]
                (K (250, FOF, "mangled_guards?") (* FUDGE *))
diff -r c76c04d876ef -r 800baa1b1406 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -612,7 +612,7 @@
   | is_type_level_monotonicity_based _ = false
 
 fun adjust_type_enc (THF _) type_enc = type_enc
-  | adjust_type_enc TFF (Simple_Types (Higher_Order, level)) =
+  | adjust_type_enc TFF (Simple_Types (_, level)) =
     Simple_Types (First_Order, level)
   | adjust_type_enc format (Simple_Types (_, level)) =
     adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))