# HG changeset patch
# User wenzelm
# Date 1308516817 -7200
# Node ID 7ab4be64575da301e0af888dc46114675fc7f0e7
# Parent  3d42dea16357ce89c7f8c2aba09343428210515b# Parent  c768f7adb7116ef57cad44a18bcc5bb56ae4a611
merged;

diff -r 3d42dea16357 -r 7ab4be64575d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Jun 19 22:53:37 2011 +0200
@@ -129,8 +129,8 @@
   | string_for_failure (UnsoundProof (true, ss)) =
     "The prover found a type-unsound proof " ^ involving ss ^
     "even though a supposedly type-sound encoding was used (or, less likely, \
-    \your axioms are inconsistent). You might want to report this to the \
-    \Isabelle developers."
+    \your axioms are inconsistent). Please report this to the Isabelle \
+    \developers."
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure Inappropriate =
diff -r 3d42dea16357 -r 7ab4be64575d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Jun 19 22:53:37 2011 +0200
@@ -213,11 +213,10 @@
       (ProofMissing, "SZS status Theorem"),
       (TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded"),
-      (OutOfResources,
-       "# Cannot determine problem status within resource limit"),
+      (OutOfResources, "# Cannot determine problem status"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>
@@ -257,7 +256,7 @@
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
-   conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
+   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>
@@ -299,7 +298,7 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],
-   conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+   conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>
diff -r 3d42dea16357 -r 7ab4be64575d src/HOL/ex/ATP_Export.thy
--- a/src/HOL/ex/ATP_Export.thy	Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/ex/ATP_Export.thy	Sun Jun 19 22:53:37 2011 +0200
@@ -4,7 +4,7 @@
 begin
 
 ML {*
-val do_it = false; (* switch to "true" to generate files *)
+val do_it = false; (* switch to "true" to generate the files *)
 val thy = @{theory Complex_Main};
 val ctxt = @{context}
 *}
diff -r 3d42dea16357 -r 7ab4be64575d src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Sun Jun 19 22:53:37 2011 +0200
@@ -8,6 +8,7 @@
 
 signature ATP_EXPORT =
 sig
+  val theorems_mentioned_in_proof_term : thm -> string list
   val generate_tptp_graph_file_for_theory :
     Proof.context -> theory -> string -> unit
   val generate_tptp_inference_file_for_theory :
@@ -25,16 +26,22 @@
   Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
                                 true [] []
 
+(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
+   fixes that seem to be missing over there; or maybe the two code portions are
+   not doing the same? *)
 fun fold_body_thms f =
   let
-    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
-      if Inttab.defined seen i then (x, seen)
-      else
-        let
-          val body' = Future.join body;
-          val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen);
-        in (x' |> n = 1 ? f (name, prop, body'), seen') end);
-  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
+    fun app n (PBody {thms, ...}) =
+      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+        if Inttab.defined seen i then
+          (x, seen)
+        else
+          let
+            val body' = Future.join body
+            val n' = n + (if name = "" then 0 else 1)
+            val (x', seen') = (x, seen) |> n' <= 1 ? app n' body'
+          in (x' |> n = 1 ? f (name, prop, body'), seen') end)
+  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
 
 fun theorems_mentioned_in_proof_term thm =
   let