# HG changeset patch
# User blanchet
# Date 1344009395 -7200
# Node ID 14b0732c72f7d47dde61f868184d097e197dfe37
# Parent  81755fd809be23de2d84a6670b039e279633289b
crank up max number of dependencies

diff -r 81755fd809be -r 14b0732c72f7 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Aug 03 17:56:35 2012 +0200
@@ -57,11 +57,6 @@
 
 val all_names = map (rpair () o nickname_of) #> Symtab.make
 
-fun smart_dependencies_of ctxt params prover facts all_names th =
-  case atp_dependencies_of ctxt params prover 0 facts all_names th of
-    SOME deps => deps
-  | NONE => isar_dependencies_of all_names th |> these
-
 fun generate_accessibility ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
@@ -129,7 +124,9 @@
     fun do_thm th =
       let
         val name = nickname_of th
-        val deps = smart_dependencies_of ctxt params prover facts all_names th
+        val deps =
+          atp_dependencies_of ctxt params prover 0 facts all_names th
+          |> snd |> these
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
@@ -143,13 +140,14 @@
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
-    val ths = facts |> map snd
-    val all_names = all_names ths
+    val all_names = all_names (map snd facts)
     fun do_fact ((_, stature), th) prevs =
       let
         val name = nickname_of th
         val feats = features_of ctxt prover thy stature [prop_of th]
-        val deps = smart_dependencies_of ctxt params prover facts all_names th
+        val deps =
+          atp_dependencies_of ctxt params prover 0 facts all_names th
+          |> snd |> these
         val kind = Thm.legacy_get_kind th
         val core =
           escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
diff -r 81755fd809be -r 14b0732c72f7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 03 17:56:35 2012 +0200
@@ -44,7 +44,7 @@
   val isar_dependencies_of : unit Symtab.table -> thm -> string list option
   val atp_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
-    -> thm -> string list option
+    -> thm -> bool * string list option
   val is_thm_technical : thm -> bool
   val mash_CLEAR : Proof.context -> unit
   val mash_ADD :
@@ -315,10 +315,10 @@
   |> scope <> Global ? cons "local"
   |> (case string_of_status status of "" => I | s => cons s)
 
-(* Too many dependencies is a sign that a decision procedure is at work. There
-   isn't much too learn from such proofs. *)
-val max_dependencies = 20
-val atp_dependency_default_max_fact = 50
+(* Too many dependencies is a sign that a crazy decision procedure is at work.
+   There isn't much to learn from such proofs. *)
+val max_dependencies = 100
+val atp_dependency_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
 val typedef_deps = [@{thm CollectI} |> nickname_of]
@@ -355,7 +355,7 @@
 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
                         auto_level facts all_names th =
   case isar_dependencies_of all_names th of
-    SOME [] => NONE
+    SOME [] => (false, SOME [])
   | isar_deps =>
     let
       val thy = Proof_Context.theory_of ctxt
@@ -372,7 +372,7 @@
         | NONE => accum (* shouldn't happen *)
       val facts =
         facts |> mepo_suggested_facts ctxt params prover
-                     (max_facts |> the_default atp_dependency_default_max_fact)
+                     (max_facts |> the_default atp_dependency_default_max_facts)
                      NONE hyp_ts concl_t
               |> fold (add_isar_dep facts) (these isar_deps)
               |> map fix_name
@@ -396,8 +396,10 @@
            end
          else
            ();
-         used_facts |> map fst |> trim_dependencies th)
-      | _ => NONE
+         case used_facts |> map fst |> trim_dependencies th of
+           NONE => (false, isar_deps)
+         | atp_deps => (true, atp_deps))
+      | _ => (false, isar_deps)
     end
 
 val technical_theories =
@@ -747,6 +749,7 @@
             SOME []
           else if atp then
             atp_dependencies_of ctxt params prover auto_level facts all_names th
+            |> (fn (false, _) => NONE | (true, deps) => deps)
           else
             isar_dependencies_of all_names th
         fun do_commit [] [] state = state