# 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))