merged
authorblanchet
Fri, 30 Jul 2010 15:03:42 +0200
changeset 38106 d44a5f602b8c
parent 38082 61280b97b761 (current diff)
parent 38105 373351f5f834 (diff)
child 38107 3a46cebd7983
child 38112 cf08f4780938
child 38121 a9d96531c2ee
merged
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -306,11 +306,11 @@
       ctxt
       |> change_dir dir
       |> Config.put Sledgehammer.measure_runtime true
-    val params = Sledgehammer_Isar.default_params thy []
+    val params = Sledgehammer_Isar.default_params thy
+      [("timeout", Int.toString timeout ^ " s")]
     val problem =
       {subgoal = 1, goal = (ctxt', (facts, goal)),
-       relevance_override = {add = [], del = [], only = false},
-       axiom_clauses = NONE, filtered_clauses = NONE}
+       relevance_override = {add = [], del = [], only = false}, axioms = NONE}
     val time_limit =
       (case hard_timeout of
         NONE => I
@@ -318,7 +318,7 @@
     val ({outcome, message, used_thm_names,
           atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time
-                      (prover params (K "") (Time.fromSeconds timeout))) problem
+                      (prover params (K ""))) problem
   in
     case outcome of
       NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
@@ -381,7 +381,6 @@
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     open Metis_Clauses
-    open Sledgehammer_Isar
     val thy = Proof.theory_of st
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_atp thy args
@@ -389,8 +388,8 @@
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
       |> the_default 5
-    val params = default_params thy
-      [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
+    val params = Sledgehammer_Isar.default_params thy
+      [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
     val minimize =
       Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -49,9 +49,10 @@
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 fun string_for_term (ATerm (s, [])) = s
+  | string_for_term (ATerm ("equal", ts)) =
+    space_implode " = " (map string_for_term ts)
   | string_for_term (ATerm (s, ts)) =
-    if s = "equal" then space_implode " = " (map string_for_term ts)
-    else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+    s ^ "(" ^ commas (map string_for_term ts) ^ ")"
 fun string_for_quantifier AForall = "!"
   | string_for_quantifier AExists = "?"
 fun string_for_connective ANot = "~"
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -13,8 +13,8 @@
     MalformedOutput | UnknownError
 
   type prover_config =
-    {executable: string * string,
-     required_executables: (string * string) list,
+    {exec: string * string,
+     required_execs: (string * string) list,
      arguments: bool -> Time.time -> string,
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
@@ -44,8 +44,8 @@
     MalformedOutput | UnknownError
 
 type prover_config =
-  {executable: string * string,
-   required_executables: (string * string) list,
+  {exec: string * string,
+   required_execs: (string * string) list,
    arguments: bool -> Time.time -> string,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
@@ -60,14 +60,14 @@
 fun string_for_failure Unprovable = "The ATP problem is unprovable."
   | string_for_failure IncompleteUnprovable =
     "The ATP cannot prove the problem."
-  | string_for_failure CantConnect = "Can't connect to remote ATP."
+  | string_for_failure CantConnect = "Can't connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
   | string_for_failure OldSpass =
-    "Warning: Isabelle requires a more recent version of SPASS with \
-    \support for the TPTP syntax. To install it, download and extract the \
-    \package \"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and \
-    \add the \"spass-3.7\" directory's absolute path to " ^
+    "Isabelle requires a more recent version of SPASS with support for the \
+    \TPTP syntax. To install it, download and extract the package \
+    \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
+    \\"spass-3.7\" directory's absolute path to " ^
     quote (Path.implode (Path.expand (Path.appends
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
@@ -76,17 +76,18 @@
   | string_for_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
   | string_for_failure MalformedInput =
-    "Internal Isabelle error: The ATP problem is malformed. Please report \
-    \this to the Isabelle developers."
-  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
-  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
+    "The ATP problem is malformed. Please report this to the Isabelle \
+    \developers."
+  | string_for_failure MalformedOutput = "The ATP output is malformed."
+  | string_for_failure UnknownError = "An unknown ATP error occurred."
 
 fun known_failure_in_output output =
   find_first (fn (_, pattern) => String.isSubstring pattern output)
   #> Option.map fst
 
 val known_perl_failures =
-  [(NoPerl, "env: perl"),
+  [(CantConnect, "HTTP error"),
+   (NoPerl, "env: perl"),
    (NoLibwwwPerl, "Can't locate HTTP")]
 
 (* named provers *)
@@ -124,8 +125,8 @@
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
 val e_config : prover_config =
-  {executable = ("E_HOME", "eproof"),
-   required_executables = [],
+  {exec = ("E_HOME", "eproof"),
+   required_execs = [],
    arguments = fn _ => fn timeout =>
      "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
      string_of_int (to_generous_secs timeout),
@@ -139,7 +140,7 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   max_new_relevant_facts_per_iter = 80 (* FIXME *),
+   max_new_relevant_facts_per_iter = 90 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 val e = ("e", e_config)
@@ -148,13 +149,13 @@
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of "hAPP". *)
 val spass_config : prover_config =
-  {executable = ("ISABELLE_ATP", "scripts/spass"),
-   required_executables = [("SPASS_HOME", "SPASS")],
+  {exec = ("ISABELLE_ATP", "scripts/spass"),
+   required_execs = [("SPASS_HOME", "SPASS")],
    (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^
-      string_of_int (to_generous_secs timeout div 2))
+      string_of_int ((to_generous_secs timeout + 1) div 2))
      |> not complete ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
@@ -165,7 +166,7 @@
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (OldSpass, "tptp2dfg")],
-   max_new_relevant_facts_per_iter = 26 (* FIXME *),
+   max_new_relevant_facts_per_iter = 35 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
 val spass = ("spass", spass_config)
@@ -173,8 +174,8 @@
 (* Vampire *)
 
 val vampire_config : prover_config =
-  {executable = ("VAMPIRE_HOME", "vampire"),
-   required_executables = [],
+  {exec = ("VAMPIRE_HOME", "vampire"),
+   required_execs = [],
    arguments = fn _ => fn timeout =>
      "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
      " --input_file ",
@@ -186,9 +187,10 @@
    known_failures =
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
+      (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found")],
-   max_new_relevant_facts_per_iter = 40 (* FIXME *),
+   max_new_relevant_facts_per_iter = 50 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 val vampire = ("vampire", vampire_config)
@@ -221,16 +223,15 @@
         ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
           prefers_theory_relevant, explicit_forall, ...} : prover_config)
         : prover_config =
-  {executable = ("ISABELLE_ATP", "scripts/remote_atp"),
-   required_executables = [],
+  {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
+   required_execs = [],
    arguments = fn _ => fn timeout =>
      " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
      the_system atp_prefix,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =
      known_failures @ known_perl_failures @
-     [(CantConnect, "HTTP-Error"),
-      (TimedOut, "says Timeout")],
+     [(TimedOut, "says Timeout")],
    max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
    prefers_theory_relevant = prefers_theory_relevant,
    explicit_forall = explicit_forall}
@@ -243,8 +244,8 @@
 val remote_e = remote_prover e "EP---"
 val remote_vampire = remote_prover vampire "Vampire---9"
 
-fun is_installed ({executable, required_executables, ...} : prover_config) =
-  forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
+fun is_installed ({exec, required_execs, ...} : prover_config) =
+  forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
 fun maybe_remote (name, config) =
   name |> not (is_installed config) ? remote_name
 
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Fri Jul 30 15:03:42 2010 +0200
@@ -98,7 +98,7 @@
 if(!$Response->is_success) {
   my $message = $Response->message;
   $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
-  print $message . "\n";
+  print "HTTP error: " . $message . "\n";
   exit(-1);
 } elsif (exists($Options{'w'})) {
   print $Response->content;
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -16,9 +16,9 @@
     TConsLit of name * name * name list |
     TVarLit of name * name
   datatype arity_clause =
-    ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   datatype class_rel_clause =
-    ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
+    ClassRelClause of {name: string, subclass: name, superclass: name}
   datatype combtyp =
     CombTVar of name |
     CombTFree of name |
@@ -84,8 +84,6 @@
 val tvar_prefix = "T_";
 val tfree_prefix = "t_";
 
-val class_rel_clause_prefix = "clsrel_";
-
 val const_prefix = "c_";
 val type_const_prefix = "tc_";
 val class_prefix = "class_";
@@ -259,7 +257,7 @@
   TVarLit of name * name
 
 datatype arity_clause =
-  ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
 
 
 fun gen_TVars 0 = []
@@ -271,12 +269,12 @@
     (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
 
 (*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
+fun make_axiom_arity_clause (tcons, name, (cls,args)) =
   let
     val tvars = gen_TVars (length args)
     val tvars_srts = ListPair.zip (tvars, args)
   in
-    ArityClause {axiom_name = axiom_name, 
+    ArityClause {name = name, 
                  conclLit = TConsLit (`make_type_class cls,
                                       `make_fixed_type_const tcons,
                                       tvars ~~ tvars),
@@ -287,7 +285,7 @@
 (**** Isabelle class relations ****)
 
 datatype class_rel_clause =
-  ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
+  ClassRelClause of {name: string, subclass: name, superclass: name}
 
 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
 fun class_pairs _ [] _ = []
@@ -299,10 +297,9 @@
       in fold add_supers subs [] end
 
 fun make_class_rel_clause (sub,super) =
-  ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^
-                               ascii_of super,
+  ClassRelClause {name = sub ^ "_" ^ super,
                   subclass = `make_type_class sub,
-                  superclass = `make_type_class super};
+                  superclass = `make_type_class super}
 
 fun make_class_rel_clauses thy subs supers =
   map make_class_rel_clause (class_pairs thy subs supers);
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -86,11 +86,11 @@
             val args   = map hol_term_to_fol_FO tms
         in Metis.Term.Fn (c, tyargs @ args) end
     | (CombVar ((v, _), _), []) => Metis.Term.Var v
-    | _ => raise Fail "hol_term_to_fol_FO";
+    | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
 
-fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
-  | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
+fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
       Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
+  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
 
@@ -764,12 +764,11 @@
                     (_,ith)::_ =>
                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
                          [ith])
-                  | _ => (trace_msg (fn () => "Metis: No result");
-                          raise METIS ("FOL_SOLVE", ""))
+                  | _ => (trace_msg (fn () => "Metis: No result"); [])
             end
         | Metis.Resolution.Satisfiable _ =>
             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
-             raise METIS ("FOL_SOLVE", ""))
+             [])
   end;
 
 val type_has_top_sort =
@@ -798,10 +797,8 @@
          if mode = HO then
            (warning ("Metis: Falling back on \"metisFT\".");
             generic_metis_tac FT ctxt ths i st0)
-         else if msg = "" then
+         else
            Seq.empty
-         else
-           raise error ("Metis (" ^ loc ^ "): " ^ msg)
 
 val metis_tac = generic_metis_tac HO
 val metisF_tac = generic_metis_tac FO
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -30,8 +30,7 @@
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
      relevance_override: relevance_override,
-     axiom_clauses: (string * thm) list option,
-     filtered_clauses: (string * thm) list option}
+     axioms: (string * thm) list option}
   type prover_result =
     {outcome: failure option,
      message: string,
@@ -41,10 +40,8 @@
      output: string,
      proof: string,
      internal_thm_names: string Vector.vector,
-     conjecture_shape: int list list,
-     filtered_clauses: (string * thm) list}
-  type prover =
-    params -> minimize_command -> Time.time -> problem -> prover_result
+     conjecture_shape: int list list}
+  type prover = params -> minimize_command -> problem -> prover_result
 
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
@@ -72,8 +69,13 @@
 
 (** The Sledgehammer **)
 
+(* Identifier to distinguish Sledgehammer from other tools using
+   "Async_Manager". *)
 val das_Tool = "Sledgehammer"
 
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
 fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
 fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
 val messages = Async_Manager.thread_messages das_Tool "ATP"
@@ -100,8 +102,7 @@
   {subgoal: int,
    goal: Proof.context * (thm list * thm),
    relevance_override: relevance_override,
-   axiom_clauses: (string * thm) list option,
-   filtered_clauses: (string * thm) list option}
+   axioms: (string * thm) list option}
 
 type prover_result =
   {outcome: failure option,
@@ -112,11 +113,9 @@
    output: string,
    proof: string,
    internal_thm_names: string Vector.vector,
-   conjecture_shape: int list list,
-   filtered_clauses: (string * thm) list}
+   conjecture_shape: int list list}
 
-type prover =
-  params -> minimize_command -> Time.time -> problem -> prover_result
+type prover = params -> minimize_command -> problem -> prover_result
 
 (* configuration attributes *)
 
@@ -163,7 +162,7 @@
 (* Clause preparation *)
 
 datatype fol_formula =
-  FOLFormula of {formula_name: string,
+  FOLFormula of {name: string,
                  kind: kind,
                  combformula: (name, combterm) formula,
                  ctypes_sorts: typ list}
@@ -175,12 +174,12 @@
     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
 
 (* ### FIXME: reintroduce
-fun make_clause_table xs =
+fun make_formula_table xs =
   fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-(* Remove existing axiom clauses from the conjecture clauses, as this can
+(* Remove existing axioms from the conjecture, as this can
    dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls ax_clauses =
-  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
+fun subtract_cls axioms =
+  filter_out (Termtab.defined (make_formula_table axioms) o prop_of)
 *)
 
 fun combformula_for_prop thy =
@@ -235,11 +234,15 @@
       | aux _ t = t
   in aux (maxidx_of_term t + 1) t end
 
-(* FIXME: Guarantee freshness *)
-fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
+fun presimplify_term thy =
+  Skip_Proof.make_thm thy
+  #> Meson.presimplify
+  #> prop_of
+
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
 fun conceal_bounds Ts t =
   subst_bounds (map (Free o apfst concealed_bound_name)
-                    (length Ts - 1 downto 0 ~~ rev Ts), t)
+                    (0 upto length Ts - 1 ~~ Ts), t)
 fun reveal_bounds Ts =
   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
                     (0 upto length Ts - 1 ~~ Ts))
@@ -281,29 +284,42 @@
            Axiom => HOLogic.true_const
          | Conjecture => HOLogic.false_const
 
-(* making axiom and conjecture clauses *)
-fun make_clause ctxt (formula_name, kind, t) =
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
+fun freeze_term t =
+  let
+    fun aux (t $ u) = aux t $ aux u
+      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+      | aux (Var ((s, i), T)) =
+        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+      | aux t = t
+  in t |> exists_subterm is_Var t ? aux end
+
+(* making axiom and conjecture formulas *)
+fun make_formula ctxt presimp (name, kind, t) =
   let
     val thy = ProofContext.theory_of ctxt
-    (* ### FIXME: perform other transformations previously done by
-       "Clausifier.to_nnf", e.g. "HOL.If" *)
     val t = t |> transform_elim_term
               |> Object_Logic.atomize_term thy
+    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
               |> extensionalize_term
+              |> presimp ? presimplify_term thy
+              |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
+              |> kind = Conjecture ? freeze_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
-    FOLFormula {formula_name = formula_name, combformula = combformula,
-                kind = kind, ctypes_sorts = ctypes_sorts}
+    FOLFormula {name = name, combformula = combformula, kind = kind,
+                ctypes_sorts = ctypes_sorts}
   end
 
-fun make_axiom_clause ctxt (name, th) =
-  (name, make_clause ctxt (name, Axiom, prop_of th))
-fun make_conjecture_clauses ctxt ts =
-  map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
+fun make_axiom ctxt presimp (name, th) =
+  (name, make_formula ctxt presimp (name, Axiom, prop_of th))
+fun make_conjectures ctxt ts =
+  map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
        (0 upto length ts - 1) ts
 
-(** Helper clauses **)
+(** Helper facts **)
 
 fun count_combterm (CombConst ((s, _), _, _)) =
     Symtab.map_entry s (Integer.add 1)
@@ -328,52 +344,40 @@
   Symtab.make (maps (maps (map (rpair 0) o fst))
                     [optional_helpers, optional_typed_helpers])
 
-fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
+fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   let
-    val ct = fold (fold count_fol_formula) [conjectures, axclauses]
-                  init_counters
+    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
     fun is_needed c = the (Symtab.lookup ct c) > 0
-    val cnfs =
-      (optional_helpers
-       |> full_types ? append optional_typed_helpers
-       |> maps (fn (ss, ths) =>
-                   if exists is_needed ss then map (`Thm.get_name_hint) ths
-                   else [])) @
-      (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
-  in map (snd o make_axiom_clause ctxt) cnfs end
+  in
+    (optional_helpers
+     |> full_types ? append optional_typed_helpers
+     |> maps (fn (ss, ths) =>
+                 if exists is_needed ss then map (`Thm.get_name_hint) ths
+                 else [])) @
+    (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+    |> map (snd o make_axiom ctxt false)
+  end
 
-fun s_not (@{const Not} $ t) = t
-  | s_not t = @{const Not} $ t
+fun meta_not t = @{const "==>"} $ t $ @{prop False}
 
-(* prepare for passing to writer,
-   create additional clauses based on the information from extra_cls *)
-fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
+fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =
   let
     val thy = ProofContext.theory_of ctxt
     val goal_t = Logic.list_implies (hyp_ts, concl_t)
     val is_FO = Meson.is_fol_term thy goal_t
-    val axtms = map (prop_of o snd) extra_cls
+    val axtms = map (prop_of o snd) axcls
     val subs = tfree_classes_of_terms [goal_t]
     val supers = tvar_classes_of_terms axtms
     val tycons = type_consts_of_terms thy (goal_t :: axtms)
-    (* TFrees in conjecture clauses; TVars in axiom clauses *)
-    val conjectures =
-      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
-        [HOLogic.dest_Trueprop concl_t]
-      |> make_conjecture_clauses ctxt
-    val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
-    val (clnames, axiom_clauses) =
-      ListPair.unzip (map (make_axiom_clause ctxt) axcls)
-    (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
-       "get_helper_clauses" call? *)
-    val helper_clauses =
-      get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
+    (* TFrees in the conjecture; TVars in the axioms *)
+    val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
+    val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls)
+    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
     (Vector.fromList clnames,
-      (conjectures, axiom_clauses, extra_clauses, helper_clauses,
-       class_rel_clauses, arity_clauses))
+      (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
   end
 
 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
@@ -397,10 +401,15 @@
         val (head, args) = strip_combterm_comb u
         val (x, ty_args) =
           case head of
-            CombConst (name, _, ty_args) =>
-            if fst name = "equal" then
+            CombConst (name as (s, s'), _, ty_args) =>
+            if s = "equal" then
               (if top_level andalso length args = 2 then name
                else ("c_fequal", @{const_name fequal}), [])
+            else if top_level then
+              case s of
+                "c_False" => (("$false", s'), [])
+              | "c_True" => (("$true", s'), [])
+              | _ => (name, if full_types then [] else ty_args)
             else
               (name, if full_types then [] else ty_args)
           | CombVar (name, _) => (name, [])
@@ -424,15 +433,14 @@
                 (type_literals_for_types ctypes_sorts))
            (formula_for_combformula full_types combformula)
 
-fun problem_line_for_axiom full_types
-        (formula as FOLFormula {formula_name, kind, ...}) =
-  Fof (axiom_prefix ^ ascii_of formula_name, kind,
-       formula_for_axiom full_types formula)
+fun problem_line_for_fact prefix full_types
+                          (formula as FOLFormula {name, kind, ...}) =
+  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
 
-fun problem_line_for_class_rel_clause
-        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+                                                       superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
-    Fof (ascii_of axiom_name, Axiom,
+    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
                            AAtom (ATerm (superclass, [ty_arg]))]))
   end
@@ -442,17 +450,17 @@
   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
     (false, ATerm (c, [ATerm (sort, [])]))
 
-fun problem_line_for_arity_clause
-        (ArityClause {axiom_name, conclLit, premLits, ...}) =
-  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+                                                ...}) =
+  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
        mk_ahorn (map (formula_for_fo_literal o apfst not
                       o fo_literal_for_arity_literal) premLits)
                 (formula_for_fo_literal
                      (fo_literal_for_arity_literal conclLit)))
 
 fun problem_line_for_conjecture full_types
-        (FOLFormula {formula_name, kind, combformula, ...}) =
-  Fof (conjecture_prefix ^ formula_name, kind,
+                                (FOLFormula {name, kind, combformula, ...}) =
+  Fof (conjecture_prefix ^ name, kind,
        formula_for_combformula full_types combformula)
 
 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
@@ -596,17 +604,18 @@
       (const_table_for_problem explicit_apply problem) problem
 
 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
-                    file (conjectures, axiom_clauses, extra_clauses,
-                          helper_clauses, class_rel_clauses, arity_clauses) =
+                    file (conjectures, axioms, helper_facts, class_rel_clauses,
+                          arity_clauses) =
   let
-    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
+    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+    val helper_lines =
+      map (problem_line_for_fact helper_prefix full_types) helper_facts
+    val conjecture_lines =
+      map (problem_line_for_conjecture full_types) conjectures
+    val tfree_lines = problem_lines_for_free_types conjectures
     val class_rel_lines =
       map problem_line_for_class_rel_clause class_rel_clauses
     val arity_lines = map problem_line_for_arity_clause arity_clauses
-    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
-    val conjecture_lines =
-      map (problem_line_for_conjecture full_types) conjectures
-    val tfree_lines = problem_lines_for_free_types conjectures
     (* Reordering these might or might not confuse the proof reconstruction
        code or the SPASS Flotter hack. *)
     val problem =
@@ -638,7 +647,8 @@
 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
 
 val parse_clause_formula_pair =
-  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id
+  --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")"
   --| Scan.option ($$ ",")
 val parse_clause_formula_relation =
   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
@@ -664,8 +674,8 @@
         |> map (fn s => find_index (curry (op =) s) seq + 1)
     in
       (conjecture_shape |> map (maps renumber_conjecture),
-       seq |> map (the o AList.lookup (op =) name_map)
-           |> map (fn s => case try (unprefix axiom_prefix) s of
+       seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the
+                                  |> try (unprefix axiom_prefix) of
                              SOME s' => undo_ascii_of s'
                            | NONE => "")
            |> Vector.fromList)
@@ -677,33 +687,29 @@
 (* generic TPTP-based provers *)
 
 fun prover_fun name
-        {executable, required_executables, arguments, proof_delims,
-         known_failures, max_new_relevant_facts_per_iter,
-         prefers_theory_relevant, explicit_forall}
+        {exec, required_execs, arguments, proof_delims, known_failures,
+         max_new_relevant_facts_per_iter, prefers_theory_relevant,
+         explicit_forall}
         ({debug, overlord, full_types, explicit_apply, relevance_threshold,
           relevance_convergence, theory_relevant, defs_relevant, isar_proof,
-          isar_shrink_factor, ...} : params)
-        minimize_command timeout
-        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
-         : problem) =
+          isar_shrink_factor, timeout, ...} : params)
+        minimize_command
+        ({subgoal, goal, relevance_override, axioms} : problem) =
   let
-    (* get clauses and prepare them for writing *)
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt
     (* ### FIXME: (1) preprocessing for "if" etc. *)
     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
-    val the_filtered_clauses =
-      case filtered_clauses of
-        SOME fcls => fcls
+    val the_axioms =
+      case axioms of
+        SOME axioms => axioms
       | NONE => relevant_facts full_types relevance_threshold
                     relevance_convergence defs_relevant
                     max_new_relevant_facts_per_iter
                     (the_default prefers_theory_relevant theory_relevant)
                     relevance_override goal hyp_ts concl_t
-    val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
-    val (internal_thm_names, clauses) =
-      prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
-                      the_filtered_clauses
+    val (internal_thm_names, formulas) =
+      prepare_formulas ctxt full_types hyp_ts concl_t the_axioms
 
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -722,7 +728,7 @@
         else error ("No such directory: " ^ the_dest_dir ^ ".")
       end;
 
-    val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)
+    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     (* write out problem file and call prover *)
     fun command_line complete probfile =
       let
@@ -746,8 +752,7 @@
         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
       in (output, as_time t) end;
     fun run_on probfile =
-      case filter (curry (op =) "" o getenv o fst)
-                  (executable :: required_executables) of
+      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
         (home_var, _) :: _ =>
         error ("The environment variable " ^ quote home_var ^ " is not set.")
       | [] =>
@@ -771,7 +776,7 @@
             val readable_names = debug andalso overlord
             val (pool, conjecture_offset) =
               write_tptp_file thy readable_names explicit_forall full_types
-                              explicit_apply probfile clauses
+                              explicit_apply probfile formulas
             val conjecture_shape =
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
               |> map single
@@ -814,8 +819,7 @@
     {outcome = outcome, message = message, pool = pool,
      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
      output = output, proof = proof, internal_thm_names = internal_thm_names,
-     conjecture_shape = conjecture_shape,
-     filtered_clauses = the_filtered_clauses}
+     conjecture_shape = conjecture_shape}
   end
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
@@ -837,10 +841,9 @@
             let
               val problem =
                 {subgoal = i, goal = (ctxt, (facts, goal)),
-                 relevance_override = relevance_override, axiom_clauses = NONE,
-                 filtered_clauses = NONE}
+                 relevance_override = relevance_override, axioms = NONE}
             in
-              prover params (minimize_command name) timeout problem |> #message
+              prover params (minimize_command name) problem |> #message
               handle ERROR message => "Error: " ^ message ^ "\n"
             end)
   end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -88,18 +88,9 @@
                      (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
 
 val fresh_prefix = "Sledgehammer.Fresh."
-
 val flip = Option.map not
-
-val boring_natural_consts = [@{const_name If}]
-(* Including equality in this list might be expected to stop rules like
-   subset_antisym from being chosen, but for some reason filtering works better
-   with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
-   because any remaining occurrences must be within comprehensions. *)
-val boring_cnf_consts =
-  [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
-   @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
-   @{const_name "op ="}]
+(* These are typically simplified away by "Meson.presimplify". *)
+val boring_consts = [@{const_name If}, @{const_name Let}]
 
 fun get_consts_typs thy pos ts =
   let
@@ -149,7 +140,7 @@
         do_term t0 #> do_formula pos t1  (* theory constant *)
       | _ => do_term t
   in
-    Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
+    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
                  |> fold (do_formula pos) ts
   end
 
@@ -213,11 +204,8 @@
              (the (Symtab.lookup const_tab c)
               handle Option.Option => raise Fail ("Const: " ^ c)) 0
 
-(*A surprising number of theorems contain only a few significant constants.
-  These include all induction rules, and other general theorems. Filtering
-  theorems in clause form reveals these complexities in the form of Skolem
-  functions. If we were instead to filter theorems in their natural form,
-  some other method of measuring theorem complexity would become necessary.*)
+(* A surprising number of theorems contain only a few significant constants.
+   These include all induction rules, and other general theorems. *)
 
 (* "log" seems best in practice. A constant function of one ignores the constant
    frequencies. *)
@@ -228,13 +216,13 @@
 
 (*Relevant constants are weighted according to frequency,
   but irrelevant constants are simply counted. Otherwise, Skolem functions,
-  which are rare, would harm a clause's chances of being picked.*)
-fun clause_weight const_tab gctyps consts_typs =
-    let val rel = filter (uni_mem gctyps) consts_typs
-        val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
-    in
-        rel_weight / (rel_weight + real (length consts_typs - length rel))
-    end;
+  which are rare, would harm a formula's chances of being picked.*)
+fun formula_weight const_tab gctyps consts_typs =
+  let
+    val rel = filter (uni_mem gctyps) consts_typs
+    val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
+    val res = rel_weight / (rel_weight + real (length consts_typs - length rel))
+  in if Real.isFinite res then res else 0.0 end
 
 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
 fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
@@ -270,13 +258,13 @@
         | _ => false
     end;
 
-type annotated_cnf_thm = (string * thm) * (string * const_typ list) list
+type annotated_thm = (string * thm) * (string * const_typ list) list
 
 (*For a reverse sort, putting the largest values first.*)
 fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
 
-(*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) =
+(* Limit the number of new facts, to prevent runaway acceptance. *)
+fun take_best max_new (newpairs : (annotated_thm * real) list) =
   let val nnew = length newpairs
   in
     if nnew <= max_new then (map #1 newpairs, [])
@@ -294,8 +282,8 @@
       end
   end;
 
-fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
-                     ({add, del, ...} : relevance_override) const_tab =
+fun relevant_facts ctxt relevance_convergence defs_relevant max_new
+                   ({add, del, ...} : relevance_override) const_tab =
   let
     val thy = ProofContext.theory_of ctxt
     val add_thms = maps (ProofContext.get_fact ctxt) add
@@ -323,7 +311,8 @@
               val weight =
                 if member Thm.eq_thm add_thms th then 1.0
                 else if member Thm.eq_thm del_thms th then 0.0
-                else clause_weight const_tab rel_const_tab consts_typs
+                else formula_weight const_tab rel_const_tab consts_typs
+val _ = (if Real.isFinite weight then () else error ("*** " ^ Real.toString weight)) (*###*)
             in
               if weight >= threshold orelse
                  (defs_relevant andalso defines thy th rel_const_tab) then
@@ -335,7 +324,7 @@
                 relevant (newrels, ax :: rejects) axs
             end
         in
-          trace_msg (fn () => "relevant_clauses, current threshold: " ^
+          trace_msg (fn () => "relevant_facts, current threshold: " ^
                               Real.toString threshold);
           relevant ([], [])
         end
@@ -353,7 +342,7 @@
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
       val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
-      val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
+      val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
       val _ =
         trace_msg (fn () => "Initial constants: " ^
                             commas (goal_const_tab
@@ -361,11 +350,11 @@
                                     |> filter (curry (op <>) [] o snd)
                                     |> map fst))
       val relevant =
-        relevant_clauses ctxt relevance_convergence defs_relevant max_new
-                         relevance_override const_tab relevance_threshold
-                         goal_const_tab
-                         (map (pair_consts_typs_axiom theory_relevant thy)
-                              axioms)
+        relevant_facts ctxt relevance_convergence defs_relevant max_new
+                       relevance_override const_tab relevance_threshold
+                       goal_const_tab
+                       (map (pair_consts_typs_axiom theory_relevant thy)
+                            axioms)
     in
       trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
       relevant
@@ -387,11 +376,9 @@
      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   end;
 
-fun make_clause_table xs =
+fun make_fact_table xs =
   fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-
-fun make_unique xs =
-  Termtab.fold (cons o snd) (make_clause_table xs) []
+fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
@@ -427,8 +414,7 @@
   | apply_depth _ = 0
 
 fun is_formula_too_complex t =
-  apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
-  formula_has_too_many_lambdas [] t
+  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
 
 val exists_sledgehammer_const =
   exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
@@ -459,7 +445,8 @@
       (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
         if Facts.is_concealed facts name orelse
            (respect_no_atp andalso is_package_def name) orelse
-           member (op =) multi_base_blacklist (Long_Name.base_name name) then
+           member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
+           String.isSuffix "_def_raw" (* FIXME: crude hack *) name then
           I
         else
           let
@@ -512,12 +499,13 @@
 (* ATP invocation methods setup                                *)
 (***************************************************************)
 
-(**** Predicates to detect unwanted clauses (prolific or likely to cause
+(**** Predicates to detect unwanted facts (prolific or likely to cause
       unsoundness) ****)
 
 (** Too general means, positive equality literal with a variable X as one operand,
   when X does not occur properly in the other operand. This rules out clearly
-  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
+  inconsistent facts such as V = a | V = b, though it by no means guarantees
+  soundness. **)
 
 fun var_occurs_in_term ix =
   let
@@ -532,6 +520,7 @@
 (*Unwanted equalities include
   (1) those between a variable that does not properly occur in the second operand,
   (2) those between a variable and a record, since these seem to be prolific "cases" thms
+  (* FIXME: still a problem? *)
 *)
 fun too_general_eqterms (Var (ix,T), t) =
     not (var_occurs_in_term ix t) orelse is_record_type T
@@ -544,14 +533,14 @@
 fun has_typed_var tycons = exists_subterm
   (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
 
-(* Clauses are forbidden to contain variables of these types. The typical reason
+(* Facts are forbidden to contain variables of these types. The typical reason
    is that they lead to unsoundness. Note that "unit" satisfies numerous
-   equations like "?x = ()". The resulting clause will have no type constraint,
+   equations like "?x = ()". The resulting clauses will have no type constraint,
    yielding false proofs. Even "bool" leads to many unsound proofs, though only
    for higher-order problems. *)
 val dangerous_types = [@{type_name unit}, @{type_name bool}];
 
-(* Clauses containing variables of type "unit" or "bool" or of the form
+(* Facts containing variables of type "unit" or "bool" or of the form
    "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
    omitted. *)
 fun is_dangerous_term _ @{prop True} = true
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -18,7 +18,7 @@
 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
 struct
 
-open Metis_Clauses
+open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct
@@ -27,44 +27,61 @@
 (* wrapper for calling external prover *)
 
 fun string_for_failure Unprovable = "Unprovable."
-  | string_for_failure IncompleteUnprovable = "Failed."
   | string_for_failure TimedOut = "Timed out."
-  | string_for_failure OutOfResources = "Failed."
-  | string_for_failure OldSpass = "Error."
-  | string_for_failure MalformedOutput = "Error."
-  | string_for_failure UnknownError = "Failed."
-fun string_for_outcome NONE = "Success."
-  | string_for_outcome (SOME failure) = string_for_failure failure
+  | string_for_failure _ = "Unknown error."
 
-fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
-                               filtered_clauses name_thms_pairs =
+fun n_theorems name_thms_pairs =
+  let val n = length name_thms_pairs in
+    string_of_int n ^ " theorem" ^ plural_s n ^
+    (if n > 0 then
+       ": " ^ space_implode " "
+                  (name_thms_pairs
+                   |> map (perhaps (try (unprefix chained_prefix)))
+                   |> sort_distinct string_ord)
+     else
+       "")
+  end
+
+fun test_theorems ({debug, verbose, overlord, atps, full_types,
+                    relevance_threshold, relevance_convergence, theory_relevant,
+                    defs_relevant, isar_proof, isar_shrink_factor,
+                    ...} : params)
+                  (prover : prover) explicit_apply timeout subgoal state
+                  name_thms_pairs =
   let
-    val num_theorems = length name_thms_pairs
     val _ =
-      priority ("Testing " ^ string_of_int num_theorems ^
-                " theorem" ^ plural_s num_theorems ^
-                (if num_theorems > 0 then
-                   ": " ^ space_implode " "
-                              (name_thms_pairs
-                               |> map fst |> sort_distinct string_ord)
-                 else
-                   "") ^ "...")
-    val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
+      priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
+    val params =
+      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
+       full_types = full_types, explicit_apply = explicit_apply,
+       relevance_threshold = relevance_threshold,
+       relevance_convergence = relevance_convergence,
+       theory_relevant = theory_relevant, defs_relevant = defs_relevant,
+       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+       timeout = timeout, minimize_timeout = timeout}
+    val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},
-      axiom_clauses = SOME name_thm_pairs,
-      filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
+      axioms = SOME axioms}
+    val result as {outcome, used_thm_names, ...} =
+      prover params (K "") problem
   in
-    prover params (K "") timeout problem
-    |> tap (fn result : prover_result =>
-         priority (string_for_outcome (#outcome result)))
+    priority (case outcome of
+                NONE =>
+                if length used_thm_names = length name_thms_pairs then
+                  "Found proof."
+                else
+                  "Found proof with " ^ n_theorems used_thm_names ^ "."
+              | SOME failure => string_for_failure failure);
+    result
   end
 
 (* minimalization of thms *)
 
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun filter_used_facts used =
+  filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
 
 fun sublinear_minimize _ [] p = p
   | sublinear_minimize test (x :: xs) (seen, result) =
@@ -75,34 +92,52 @@
                          (filter_used_facts used_thm_names seen, result)
     | _ => sublinear_minimize test xs (x :: seen, result)
 
-fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
-                                  isar_proof, isar_shrink_factor, ...})
-                      i n state name_thms_pairs =
+(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
+   preprocessing time is included in the estimate below but isn't part of the
+   timeout. *)
+val fudge_msecs = 250
+
+fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
+  | minimize_theorems
+        (params as {debug, verbose, overlord, atps as atp :: _, full_types,
+                    relevance_threshold, relevance_convergence, theory_relevant,
+                    defs_relevant, isar_proof, isar_shrink_factor,
+                    minimize_timeout, ...})
+        i n state name_thms_pairs =
   let
     val thy = Proof.theory_of state
-    val prover = case atps of
-                   [atp_name] => get_prover_fun thy atp_name
-                 | _ => error "Expected a single ATP."
+    val prover = get_prover_fun thy atp
     val msecs = Time.toMilliseconds minimize_timeout
     val _ =
-      priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
+      priority ("Sledgehammer minimizer: ATP " ^ quote atp ^
                 " with a time limit of " ^ string_of_int msecs ^ " ms.")
-    val test_facts =
-      sledgehammer_test_theorems params prover minimize_timeout i state
-    val {context = ctxt, goal, ...} = Proof.goal state;
+    val {context = ctxt, goal, ...} = Proof.goal state
+    val (_, hyp_ts, concl_t) = strip_subgoal goal i
+    val explicit_apply =
+      not (forall (Meson.is_fol_term thy)
+                  (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
+    fun do_test timeout =
+      test_theorems params prover explicit_apply timeout i state
+    val timer = Timer.startRealTimer ()
   in
-    (* try prove first to check result and get used theorems *)
-    (case test_facts NONE name_thms_pairs of
-       result as {outcome = NONE, pool, proof, used_thm_names,
-                  conjecture_shape, filtered_clauses, ...} =>
+    (case do_test minimize_timeout name_thms_pairs of
+       result as {outcome = NONE, pool, used_thm_names,
+                  conjecture_shape, ...} =>
        let
+         val time = Timer.checkRealTimer timer
+         val new_timeout =
+           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
+           |> Time.fromMilliseconds
          val (min_thms, {proof, internal_thm_names, ...}) =
-           sublinear_minimize (test_facts (SOME filtered_clauses))
-                              (filter_used_facts used_thm_names name_thms_pairs)
-                              ([], result)
-         val m = length min_thms
+           sublinear_minimize (do_test new_timeout)
+               (filter_used_facts used_thm_names name_thms_pairs) ([], result)
+         val n = length min_thms
          val _ = priority (cat_lines
-           ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
+           ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+            (case filter (String.isPrefix chained_prefix o fst) min_thms of
+               [] => ""
+             | chained => " (including " ^ Int.toString (length chained) ^
+                          " chained)") ^ ".")
        in
          (SOME min_thms,
           proof_text isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -88,8 +88,8 @@
    ("no_isar_proof", "isar_proof")]
 
 val params_for_minimize =
-  ["debug", "verbose", "overlord", "full_types", "explicit_apply",
-   "isar_proof", "isar_shrink_factor", "minimize_timeout"]
+  ["debug", "verbose", "overlord", "full_types", "isar_proof",
+   "isar_shrink_factor", "minimize_timeout"]
 
 val property_dependent_params = ["atps", "full_types", "timeout"]
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -12,6 +12,8 @@
 
   val axiom_prefix : string
   val conjecture_prefix : string
+  val helper_prefix : string
+  val class_rel_clause_prefix : string
   val arity_clause_prefix : string
   val tfrees_name : string
   val metis_line: bool -> int -> int -> string list -> string
@@ -40,7 +42,9 @@
 
 val axiom_prefix = "ax_"
 val conjecture_prefix = "conj_"
-val arity_clause_prefix = "clsarity_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "clrel_";
+val arity_clause_prefix = "arity_"
 val tfrees_name = "tfrees"
 
 (* Simple simplifications to ensure that sort annotations don't leave a trail of
@@ -67,10 +71,10 @@
 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
 
 fun index_in_shape x = find_index (exists (curry (op =) x))
-fun is_axiom_clause_number thm_names num =
+fun is_axiom_number thm_names num =
   num > 0 andalso num <= Vector.length thm_names andalso
   Vector.sub (thm_names, num - 1) <> ""
-fun is_conjecture_clause_number conjecture_shape num =
+fun is_conjecture_number conjecture_shape num =
   index_in_shape num conjecture_shape >= 0
 
 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
@@ -281,7 +285,7 @@
     (SOME b, [T]) => (pos, b, T)
   | _ => raise FO_TERM [u]
 
-(** Accumulate type constraints in a clause: negative type literals **)
+(** Accumulate type constraints in a formula: negative type literals **)
 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
@@ -407,8 +411,8 @@
   | frees as (_, free_T) :: _ =>
     Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
 
-(* Interpret a list of syntax trees as a clause, extracting sort constraints
-   as they appear in the formula. *)
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
+   appear in the formula. *)
 fun prop_from_formula thy full_types tfrees phi =
   let
     fun do_formula pos phi =
@@ -484,13 +488,13 @@
   | replace_deps_in_line p (Inference (num, t, deps)) =
     Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
 
-(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
-  only in type information.*)
+(* Discard axioms; consolidate adjacent lines that prove the same formula, since
+   they differ only in type information.*)
 fun add_line _ _ (line as Definition _) lines = line :: lines
   | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
-    (* No dependencies: axiom, conjecture clause, or internal axioms or
-       definitions (Vampire). *)
-    if is_axiom_clause_number thm_names num then
+    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
+       definitions. *)
+    if is_axiom_number thm_names num then
       (* Axioms are not proof lines. *)
       if is_only_type_information t then
         map (replace_deps_in_line (num, [])) lines
@@ -499,8 +503,8 @@
         (_, []) => lines (*no repetition of proof line*)
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
-    else if is_conjecture_clause_number conjecture_shape num then
-      Inference (num, t, []) :: lines
+    else if is_conjecture_number conjecture_shape num then
+      Inference (num, negate_term t, []) :: lines
     else
       map (replace_deps_in_line (num, [])) lines
   | add_line _ _ (Inference (num, t, deps)) lines =
@@ -539,8 +543,8 @@
   | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
                      (Inference (num, t, deps)) (j, lines) =
     (j + 1,
-     if is_axiom_clause_number thm_names num orelse
-        is_conjecture_clause_number conjecture_shape num orelse
+     if is_axiom_number thm_names num orelse
+        is_conjecture_number conjecture_shape num orelse
         (not (is_only_type_information t) andalso
          null (Term.add_tvars t []) andalso
          not (exists_subterm (is_bad_free frees) t) andalso
@@ -562,10 +566,8 @@
   let
     fun axiom_name num =
       let val j = Int.fromString num |> the_default ~1 in
-        if is_axiom_clause_number thm_names j then
-          SOME (Vector.sub (thm_names, j - 1))
-        else
-          NONE
+        if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1))
+        else NONE
       end
     val tokens_of =
       String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
@@ -655,7 +657,7 @@
   | smart_case_split proofs facts = CaseSplit (proofs, facts)
 
 fun add_fact_from_dep thm_names num =
-  if is_axiom_clause_number thm_names num then
+  if is_axiom_number thm_names num then
     apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
   else
     apfst (insert (op =) (raw_prefix, num))
--- a/src/HOL/Tools/meson.ML	Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Jul 30 15:03:42 2010 +0200
@@ -14,6 +14,7 @@
   val too_many_clauses: Proof.context option -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
+  val presimplify: thm -> thm
   val make_nnf: Proof.context -> thm -> thm
   val skolemize: Proof.context -> thm -> thm
   val is_fol_term: theory -> term -> bool
@@ -389,10 +390,13 @@
 
 fun sort_clauses ths = sort (make_ord fewerlits) ths;
 
-(*True if the given type contains bool anywhere*)
-fun has_bool (Type("bool",_)) = true
-  | has_bool (Type(_, Ts)) = exists has_bool Ts
-  | has_bool _ = false;
+fun has_bool @{typ bool} = true
+  | has_bool (Type (_, Ts)) = exists has_bool Ts
+  | has_bool _ = false
+
+fun has_fun (Type (@{type_name fun}, _)) = true
+  | has_fun (Type (_, Ts)) = exists has_fun Ts
+  | has_fun _ = false
 
 (*Is the string the name of a connective? Really only | and Not can remain,
   since this code expects to be called on a clause form.*)
@@ -404,7 +408,7 @@
   of any argument contains bool.*)
 val has_bool_arg_const =
     exists_Const
-      (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
+      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
 
 (*A higher-order instance of a first-order constant? Example is the definition of
   one, 1, at a function type in theory SetsAndFunctions.*)
@@ -417,8 +421,9 @@
   Also rejects functions whose arguments are Booleans or other functions.*)
 fun is_fol_term thy t =
     Term.is_first_order ["all","All","Ex"] t andalso
-    not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t  orelse
-         has_bool_arg_const t  orelse
+    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
+                           | _ => false) t orelse
+         has_bool_arg_const t orelse
          exists_Const (higher_inst_const thy) t orelse
          has_meta_conn t);
 
@@ -529,9 +534,12 @@
   HOL_basic_ss addsimps nnf_extra_simps
     addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
 
+val presimplify =
+  rewrite_rule (map safe_mk_meta_eq nnf_simps)
+  #> simplify nnf_ss
+
 fun make_nnf ctxt th = case prems_of th of
-    [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
-             |> simplify nnf_ss
+    [] => th |> presimplify
              |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);