# HG changeset patch
# User blanchet
# Date 1368988879 -7200
# Node ID 0e70511cbba91a57584471d44b1f940064732d4f
# Parent  fd497099f5f51d5a48ff2b18ec14ab4133c02272
made "completish" mode a bit more complete

diff -r fd497099f5f5 -r 0e70511cbba9 src/HOL/TPTP/atp_problem_import.ML
--- 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 =
diff -r fd497099f5f5 -r 0e70511cbba9 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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))
diff -r fd497099f5f5 -r 0e70511cbba9 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 =