--- a/src/HOL/TPTP/atp_problem_import.ML Sun May 19 20:15:00 2013 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Sun May 19 20:41:19 2013 +0200
@@ -182,6 +182,7 @@
let
val ctxt =
ctxt |> Config.put Sledgehammer_Provers.completish (completeness > 0)
+ fun ref_of th = (Facts.named (Thm.derivation_name th), [])
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
([("debug", if debug then "true" else "false"),
@@ -190,13 +191,11 @@
("timeout", string_of_int timeout)] @
(if completeness > 0 then
[("type_enc",
- if completeness = 1 then "mono_native" else "poly_guards??"),
- ("slicing", "false")]
+ if completeness = 1 then "mono_native" else "poly_tags")]
else
[]) @
override_params)
- {add = [(Facts.named (Thm.derivation_name ext), [])],
- del = [], only = true}
+ {add = map ref_of [ext, @{thm someI}], del = [], only = true}
end
fun sledgehammer_tac demo ctxt timeout i =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun May 19 20:15:00 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun May 19 20:41:19 2013 +0200
@@ -1749,11 +1749,12 @@
|> map (apsnd (map (apsnd zero_var_indexes)))
val completish_helper_table =
- base_helper_table @
+ helper_table @
[((predicator_name, true),
@{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
((app_op_name, true),
- [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
+ [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast}),
+ (General, @{lemma "EX p. (p x <-> p y) --> x = y" by blast})]),
(("fconj", false),
@{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
(("fdisj", false),
@@ -1806,6 +1807,7 @@
fun could_specialize_helpers type_enc =
not (is_type_enc_polymorphic type_enc) andalso
level_of_type_enc type_enc <> No_Types
+
fun should_specialize_helper type_enc t =
could_specialize_helpers type_enc andalso
not (null (Term.hidden_polymorphism t))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun May 19 20:15:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun May 19 20:41:19 2013 +0200
@@ -657,7 +657,7 @@
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
val typedef_dep = nickname_of_thm @{thm CollectI}
(* Mysterious parts of the class machinery create lots of proofs that refer
- exclusively to "someI_e" (and to some internal constructions). *)
+ exclusively to "someI_ex" (and to some internal constructions). *)
val class_some_dep = nickname_of_thm @{thm someI_ex}
val fundef_ths =