--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
@@ -1040,7 +1040,7 @@
else
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- val reconstructor = if full_types then MetisX else Metis
+ val reconstructor = if full_types then MetisFT else Metis
fun do_facts (ls, ss) =
reconstructor_command reconstructor 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200
@@ -20,8 +20,8 @@
val new_skolemizer : bool Config.T
val metis_tac : Proof.context -> thm list -> int -> tactic
val metisF_tac : Proof.context -> thm list -> int -> tactic
+ val metisH_tac : Proof.context -> thm list -> int -> tactic
val metisFT_tac : Proof.context -> thm list -> int -> tactic
- val metisHO_tac : Proof.context -> thm list -> int -> tactic
val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic
val setup : theory -> theory
end
@@ -206,16 +206,16 @@
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
end
-val metis_modes = [HO, MX]
-val metisF_modes = [FO, MX]
+val metis_modes = [HO, FT]
+val metisF_modes = [FO, FT]
+val metisH_modes = [HO]
val metisFT_modes = [FT]
-val metisHO_modes = [HO]
val metisX_modes = [MX]
val metis_tac = generic_metis_tac metis_modes NONE
val metisF_tac = generic_metis_tac metisF_modes NONE
+val metisH_tac = generic_metis_tac metisH_modes NONE
val metisFT_tac = generic_metis_tac metisFT_modes NONE
-val metisHO_tac = generic_metis_tac metisHO_modes NONE
fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200
@@ -346,7 +346,8 @@
end
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
-val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
+(* FIXME: put in "Metis_Tactics" as string *)
+val default_type_sys = Preds (Polymorphic, Const_Arg_Types, Lightweight)
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200
@@ -417,7 +417,7 @@
val full_tac = Method.insert_tac facts i THEN tac ctxt i
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
-fun tac_for_reconstructor Metis = Metis_Tactics.metisHO_tac
+fun tac_for_reconstructor Metis = Metis_Tactics.metisH_tac
| tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
| tac_for_reconstructor MetisX =
(fn ctxt => Metis_Tactics.metisX_tac ctxt NONE)
@@ -790,7 +790,7 @@
|> map snd
in
play_one_line_proof debug preplay_timeout used_ths state subgoal
- [Metis, MetisX]
+ [Metis, MetisFT]
end,
fn preplay =>
let
@@ -984,7 +984,7 @@
else "smt_solver = " ^ maybe_quote name
in
case play_one_line_proof debug preplay_timeout used_ths state
- subgoal [Metis, MetisX] of
+ subgoal [Metis, MetisFT] of
p as Played _ => p
| _ => Trust_Playable (SMT (smt_settings ()), NONE)
end,