fixed TFF slicing
authorblanchet
Tue Aug 23 14:44:19 2011 +0200 (2011-08-23)
changeset 44418800baa1b1406
parent 44417 c76c04d876ef
child 44419 a460810d743e
fixed TFF slicing
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
     1.3 @@ -449,8 +449,7 @@
     1.4    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
     1.5                 (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
     1.6  val remote_vampire =
     1.7 -  remotify_atp vampire "Vampire" ["1.8"]
     1.8 -               (K (200, TFF, "mangled_guards?") (* FUDGE *))
     1.9 +  remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
    1.10  val remote_z3_atp =
    1.11    remotify_atp z3_atp "Z3" ["2.18"]
    1.12                 (K (250, FOF, "mangled_guards?") (* FUDGE *))
     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
     2.3 @@ -612,7 +612,7 @@
     2.4    | is_type_level_monotonicity_based _ = false
     2.5  
     2.6  fun adjust_type_enc (THF _) type_enc = type_enc
     2.7 -  | adjust_type_enc TFF (Simple_Types (Higher_Order, level)) =
     2.8 +  | adjust_type_enc TFF (Simple_Types (_, level)) =
     2.9      Simple_Types (First_Order, level)
    2.10    | adjust_type_enc format (Simple_Types (_, level)) =
    2.11      adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))