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