# HG changeset patch
# User blanchet
# Date 1280232135 -7200
# Node ID ae3df22dd70b93b0da725c0f24cffa679adca12a
# Parent  ada7d21fde114f151149845752898723f327574e# Parent  34e1ac9cb71d895830e216c10817fe2eca3e82aa
merged

diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -324,8 +324,7 @@
       NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     | SOME _ => (message, SH_FAIL (time_isa, time_atp))
   end
-  handle ATP_Manager.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
-       | ERROR msg => ("error: " ^ msg, SH_ERROR)
+  handle ERROR msg => ("error: " ^ msg, SH_ERROR)
        | TimeLimit.TimeOut => ("timeout", SH_ERROR)
 
 fun thms_of_name ctxt name =
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/ATP_Manager/SPASS_TPTP
--- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Tue Jul 27 14:02:15 2010 +0200
@@ -14,5 +14,6 @@
     > $name.cnf.dfg
 rm -f $name.fof.dfg
 cat $name.cnf.dfg
-$SPASS_HOME/SPASS $options $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg \
+    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
 rm -f $name.cnf.dfg
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -29,8 +29,8 @@
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
      relevance_override: relevance_override,
-     axiom_clauses: ((string * int) * thm) list option,
-     filtered_clauses: ((string * int) * thm) list option}
+     axiom_clauses: (string * thm) list option,
+     filtered_clauses: (string * thm) list option}
   datatype failure =
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
     OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
@@ -43,11 +43,10 @@
      output: string,
      proof: string,
      internal_thm_names: string Vector.vector,
-     conjecture_shape: int list list,
-     filtered_clauses: ((string * int) * thm) list}
+     conjecture_shape: int list,
+     filtered_clauses: (string * thm) list}
   type prover =
     params -> minimize_command -> Time.time -> problem -> prover_result
-  exception TRIVIAL of unit
 
   val kill_atps: unit -> unit
   val running_atps: unit -> unit
@@ -97,8 +96,8 @@
   {subgoal: int,
    goal: Proof.context * (thm list * thm),
    relevance_override: relevance_override,
-   axiom_clauses: ((string * int) * thm) list option,
-   filtered_clauses: ((string * int) * thm) list option}
+   axiom_clauses: (string * thm) list option,
+   filtered_clauses: (string * thm) list option}
 
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
@@ -113,15 +112,12 @@
    output: string,
    proof: string,
    internal_thm_names: string Vector.vector,
-   conjecture_shape: int list list,
-   filtered_clauses: ((string * int) * thm) list}
+   conjecture_shape: int list,
+   filtered_clauses: (string * thm) list}
 
 type prover =
   params -> minimize_command -> Time.time -> problem -> prover_result
 
-(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL of unit
-
 (* named provers *)
 
 structure Data = Theory_Data
@@ -168,8 +164,7 @@
                  filtered_clauses = NONE}
             in
               prover params (minimize_command name) timeout problem |> #message
-              handle TRIVIAL () => metis_line full_types i n []
-                   | ERROR message => "Error: " ^ message ^ "\n"
+              handle ERROR message => "Error: " ^ message ^ "\n"
             end)
   end
 
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -51,8 +51,9 @@
    arguments: bool -> Time.time -> string,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
-   max_axiom_clauses: int,
-   prefers_theory_relevant: bool};
+   max_new_relevant_facts_per_iter: int,
+   prefers_theory_relevant: bool,
+   explicit_forall: bool}
 
 
 (* basic template *)
@@ -99,7 +100,7 @@
   | string_for_failure OutOfResources = "The ATP ran out of resources."
   | string_for_failure OldSpass =
     (* FIXME: Change the error message below to point to the Isabelle download
-       page once the package is there (around the Isabelle2010 release). *)
+       page once the package is there. *)
     "Warning: Sledgehammer requires a more recent version of SPASS with \
     \support for the TPTP syntax. To install it, download and untar the \
     \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
@@ -114,13 +115,6 @@
   | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
 
-fun shape_of_clauses _ [] = []
-  | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
-  | shape_of_clauses j ((_ :: lits) :: clauses) =
-    let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
-      (j :: hd shape) :: tl shape
-    end
-
 
 (* Clause preparation *)
 
@@ -132,105 +126,192 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
 
-fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
-    c = (if pos then "c_False" else "c_True")
-  | is_false_literal _ = false
-fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
-      (pol andalso c = "c_True") orelse
-      (not pol andalso c = "c_False")
-  | is_true_literal _ = false;
-fun is_tautology (FOLClause {literals,...}) = exists is_true_literal literals
+fun combformula_for_prop thy =
+  let
+    val do_term = combterm_from_term thy
+    fun do_quant bs q s T t' =
+      do_formula ((s, T) :: bs) t'
+      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+    and do_conn bs c t1 t2 =
+      do_formula bs t1 ##>> do_formula bs t2
+      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
+    and do_formula bs t =
+      case t of
+        @{const Not} $ t1 =>
+        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+        do_quant bs AForall s T t'
+      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+        do_quant bs AExists s T t'
+      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
+      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
+      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+        do_conn bs AIff t1 t2
+      | _ => (fn ts => do_term bs (Envir.eta_contract t)
+                       |>> APred ||> union (op =) ts)
+  in do_formula [] end
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+   predicate variable. Leaves other theorems unchanged. We simply instantiate
+   the conclusion variable to False. (Cf. "transform_elim_term" in
+   "ATP_Systems".) *)
+(* FIXME: test! *)
+fun transform_elim_term t =
+  case Logic.strip_imp_concl t of
+    @{const Trueprop} $ Var (z, @{typ bool}) =>
+    subst_Vars [(z, @{const True})] t
+  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
+  | _ => t
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+   (Cf. "extensionalize_theorem" in "Clausifier".) *)
+fun extensionalize_term t =
+  let
+    fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
+               $ t2 $ Abs (s, var_T, t')) =
+        let val var_t = Var (("x", j), var_T) in
+          Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
+            $ betapply (t2, var_t) $ subst_bound (var_t, t')
+          |> aux (j + 1)
+        end
+      | 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 conceal_bounds Ts t =
+  subst_bounds (map (Free o apfst concealed_bound_name)
+                    (length Ts - 1 downto 0 ~~ rev 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))
+
+fun introduce_combinators_in_term ctxt kind t =
+  let
+    val thy = ProofContext.theory_of ctxt
+    fun aux Ts t =
+      case t of
+        @{const Not} $ t1 => @{const Not} $ aux Ts t1
+      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+        t0 $ Abs (s, T, aux (T :: Ts) t')
+      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+        t0 $ Abs (s, T, aux (T :: Ts) t')
+      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+          $ t1 $ t2 =>
+        t0 $ aux Ts t1 $ aux Ts t2
+      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+               t
+             else
+               let
+                 val t = t |> conceal_bounds Ts
+                           |> Envir.eta_contract
+                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
+               in
+                 t |> cterm_of thy
+                   |> Clausifier.introduce_combinators_in_cterm
+                   |> singleton (Variable.export ctxt' ctxt)
+                   |> prop_of |> Logic.dest_equals |> snd
+                   |> reveal_bounds Ts
+               end
+  in t |> not (Meson.is_fol_term thy t) ? aux [] end
+  handle THM _ =>
+         (* A type variable of sort "{}" will make abstraction fail. *)
+         case kind of
+           Axiom => HOLogic.true_const
+         | Conjecture => HOLogic.false_const
 
 (* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
+fun make_clause ctxt (formula_name, kind, t) =
   let
-    val (skolems, t) = th |> prop_of |> conceal_skolem_terms clause_id skolems
-    val (lits, ctypes_sorts) = literals_of_term thy t
+    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
+              |> extensionalize_term
+              |> introduce_combinators_in_term ctxt kind
+    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
-    if forall is_false_literal lits then
-      raise TRIVIAL ()
-    else
-      (skolems,
-       FOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
-                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
+    FOLFormula {formula_name = formula_name, combformula = combformula,
+                kind = kind, ctypes_sorts = ctypes_sorts}
   end
 
-fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
-  let
-    val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
-  in (skolems, clss |> not (is_tautology cls) ? cons (name, cls)) end
-
-fun make_axiom_clauses thy clauses =
-  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
-
-fun make_conjecture_clauses thy =
-  let
-    fun aux _ _ [] = []
-      | aux n skolems (th :: ths) =
-        let
-          val (skolems, cls) =
-            make_clause thy (n, "conjecture", Conjecture, th) skolems
-        in cls :: aux (n + 1) skolems ths end
-  in aux 0 [] 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))
+       (0 upto length ts - 1) ts
 
 (** Helper clauses **)
 
-fun count_combterm (CombConst ((c, _), _, _)) =
-    Symtab.map_entry c (Integer.add 1)
+fun count_combterm (CombConst ((s, _), _, _)) =
+    Symtab.map_entry s (Integer.add 1)
   | count_combterm (CombVar _) = I
-  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (FOLLiteral (_, t)) = count_combterm t
-fun count_clause (FOLClause {literals, ...}) = fold count_literal literals
-
-fun cnf_helper_thms thy raw =
-  map (`Thm.get_name_hint)
-  #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
+  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
+fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
+  | count_combformula (AConn (_, phis)) = fold count_combformula phis
+  | count_combformula (APred tm) = count_combterm tm
+fun count_fol_formula (FOLFormula {combformula, ...}) =
+  count_combformula combformula
 
 val optional_helpers =
-  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
-   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
-   (["c_COMBS"], (false, @{thms COMBS_def}))]
+  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
+   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+   (["c_COMBS"], @{thms COMBS_def})]
 val optional_typed_helpers =
-  [(["c_True", "c_False"], (true, @{thms True_or_False})),
-   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+  [(["c_True", "c_False"], @{thms True_or_False}),
+   (["c_If"], @{thms if_True if_False True_or_False})]
 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
 
 val init_counters =
   Symtab.make (maps (maps (map (rpair 0) o fst))
                     [optional_helpers, optional_typed_helpers])
 
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
+fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
   let
-    val axclauses = map snd (make_axiom_clauses thy axcls)
-    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+    val ct = fold (fold count_fol_formula) [conjectures, axclauses]
+                  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, (raw, ths)) =>
-                   if exists is_needed ss then cnf_helper_thms thy raw ths
-                   else []))
-      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
-  in map snd (make_axiom_clauses thy cnfs) end
+       |> 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
+
+fun s_not (@{const Not} $ t) = t
+  | s_not t = @{const Not} $ t
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses full_types goal_cls axcls extra_cls thy =
+fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
   let
-    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
-    val ccls = subtract_cls extra_cls goal_cls
-    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
-    val ccltms = map prop_of ccls
-    and axtms = map (prop_of o snd) extra_cls
-    val subs = tfree_classes_of_terms ccltms
-    and supers = tvar_classes_of_terms axtms
-    and tycons = type_consts_of_terms thy (ccltms @ axtms)
-    (*TFrees in conjecture clauses; TVars in axiom clauses*)
-    val conjectures = make_conjecture_clauses thy ccls
-    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
-    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
+    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 _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t)
+    val axtms = map (prop_of o snd) extra_cls
+    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 thy is_FO full_types conjectures extra_cls
+      get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
@@ -261,27 +342,38 @@
   #> snd #> Substring.string #> strip_spaces #> explode
   #> parse_clause_formula_relation #> fst
 
-fun repair_theorem_names output thm_names =
+fun repair_conjecture_shape_and_theorem_names output conjecture_shape
+                                              thm_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
+    (* This is a hack required for keeping track of axioms after they have been
+       clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
+       of this hack. *)
     let
+      val j0 = hd conjecture_shape
       val seq = extract_clause_sequence output
       val name_map = extract_clause_formula_relation output
+      fun renumber_conjecture j =
+        AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
+        |> the_single
+        |> (fn s => find_index (curry (op =) s) seq + 1)
     in
-      seq |> map (the o AList.lookup (op =) name_map)
-          |> map (fn s => case try (unprefix axiom_prefix) s of
-                            SOME s' => undo_ascii_of s'
-                          | NONE => "")
-          |> Vector.fromList
+      (conjecture_shape |> map renumber_conjecture,
+       seq |> map (the o AList.lookup (op =) name_map)
+           |> map (fn s => case try (unprefix axiom_prefix) s of
+                             SOME s' => undo_ascii_of s'
+                           | NONE => "")
+           |> Vector.fromList)
     end
   else
-    thm_names
+    (conjecture_shape, thm_names)
 
 
 (* generic TPTP-based provers *)
 
 fun generic_tptp_prover
         (name, {home_var, executable, arguments, proof_delims, known_failures,
-                max_axiom_clauses, prefers_theory_relevant})
+                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)
@@ -291,21 +383,21 @@
   let
     (* get clauses and prepare them for writing *)
     val (ctxt, (_, th)) = goal;
-    val thy = ProofContext.theory_of ctxt;
-    val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
-    val goal_cls = List.concat goal_clss
+    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
       | NONE => relevant_facts full_types relevance_threshold
-                    relevance_convergence defs_relevant max_axiom_clauses
+                    relevance_convergence defs_relevant
+                    max_new_relevant_facts_per_iter
                     (the_default prefers_theory_relevant theory_relevant)
-                    relevance_override goal goal_cls
-                |> Clausifier.cnf_rules_pairs thy true
+                    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 full_types goal_cls the_axiom_clauses the_filtered_clauses
-                      thy
+      prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
+                      the_filtered_clauses
 
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -370,9 +462,10 @@
             in (output, msecs, proof, outcome) end
           val readable_names = debug andalso overlord
           val (pool, conjecture_offset) =
-            write_tptp_file thy readable_names full_types explicit_apply
-                            probfile clauses
-          val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
+            write_tptp_file thy readable_names explicit_forall full_types
+                            explicit_apply probfile clauses
+          val conjecture_shape =
+            conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
           val result =
             do_run false
             |> (fn (_, msecs0, _, SOME _) =>
@@ -396,7 +489,9 @@
 
     val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
       with_path cleanup export run_on (prob_pathname subgoal)
-    val internal_thm_names = repair_theorem_names output internal_thm_names
+    val (conjecture_shape, internal_thm_names) =
+      repair_conjecture_shape_and_theorem_names output conjecture_shape
+                                                internal_thm_names
 
     val (message, relevant_thm_names) =
       case outcome of
@@ -431,16 +526,17 @@
      string_of_int (to_generous_secs timeout),
    proof_delims = [tstp_proof_delims],
    known_failures =
-     [(Unprovable, "SZS status: Satisfiable"),
-      (Unprovable, "SZS status Satisfiable"),
+     [(Unprovable, "SZS status: CounterSatisfiable"),
+      (Unprovable, "SZS status CounterSatisfiable"),
       (TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded"),
       (OutOfResources,
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   max_axiom_clauses = 100,
-   prefers_theory_relevant = false}
+   max_new_relevant_facts_per_iter = 80 (* FIXME *),
+   prefers_theory_relevant = false,
+   explicit_forall = false}
 val e = tptp_prover "e" e_config
 
 
@@ -463,8 +559,9 @@
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (OldSpass, "tptp2dfg")],
-   max_axiom_clauses = 40,
-   prefers_theory_relevant = true}
+   max_new_relevant_facts_per_iter = 26 (* FIXME *),
+   prefers_theory_relevant = true,
+   explicit_forall = true}
 val spass = tptp_prover "spass" spass_config
 
 (* Vampire *)
@@ -484,8 +581,9 @@
       (IncompleteUnprovable, "CANNOT PROVE"),
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found")],
-   max_axiom_clauses = 60,
-   prefers_theory_relevant = false}
+   max_new_relevant_facts_per_iter = 40 (* FIXME *),
+   prefers_theory_relevant = false,
+   explicit_forall = false}
 val vampire = tptp_prover "vampire" vampire_config
 
 (* Remote prover invocation via SystemOnTPTP *)
@@ -517,8 +615,9 @@
    (MalformedOutput, "Remote script could not extract proof")]
 
 fun remote_config atp_prefix args
-        ({proof_delims, known_failures, max_axiom_clauses,
-          prefers_theory_relevant, ...} : prover_config) : prover_config =
+        ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
+          prefers_theory_relevant, explicit_forall, ...} : prover_config)
+        : prover_config =
   {home_var = "ISABELLE_ATP_MANAGER",
    executable = "SystemOnTPTP",
    arguments = fn _ => fn timeout =>
@@ -526,8 +625,9 @@
      the_system atp_prefix,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures = remote_known_failures @ known_failures,
-   max_axiom_clauses = max_axiom_clauses,
-   prefers_theory_relevant = prefers_theory_relevant}
+   max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
+   prefers_theory_relevant = prefers_theory_relevant,
+   explicit_forall = explicit_forall}
 
 fun remote_tptp_prover prover atp_prefix args config =
   tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -7,12 +7,11 @@
 
 signature CLAUSIFIER =
 sig
+  val introduce_combinators_in_cterm : cterm -> thm
   val cnf_axiom: theory -> bool -> thm -> thm list
   val cnf_rules_pairs :
     theory -> bool -> (string * thm) list -> ((string * int) * thm) list
   val neg_clausify: thm -> thm list
-  val neg_conjecture_clauses:
-    Proof.context -> thm -> int -> thm list list * (string * typ) list
 end;
 
 structure Clausifier : CLAUSIFIER =
@@ -23,16 +22,17 @@
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
 val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
 
-(*Converts an elim-rule into an equivalent theorem that does not have the
-  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
-  conclusion variable to False.*)
-fun transform_elim th =
+(* Converts an elim-rule into an equivalent theorem that does not have the
+   predicate variable. Leaves other theorems unchanged. We simply instantiate
+   the conclusion variable to False. (Cf. "transform_elim_term" in
+   "ATP_Systems".) *)
+fun transform_elim_theorem th =
   case concl_of th of    (*conclusion variable*)
        @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
     | v as Var(_, @{typ prop}) =>
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
-    | _ => th;
+    | _ => th
 
 (*To enforce single-threading*)
 exception Clausify_failure of theory;
@@ -84,11 +84,13 @@
 
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
-(* Removes the lambdas from an equation of the form t = (%x. u). *)
-fun extensionalize th =
+(* ### FIXME: removes only one lambda? *)
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+   (Cf. "extensionalize_term" in "ATP_Systems".) *)
+fun extensionalize_theorem th =
   case prop_of th of
     _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
-         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+         $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
   | _ => th
 
 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
@@ -107,8 +109,11 @@
       val thy = theory_of_cterm ct
       val Abs(x,_,body) = term_of ct
       val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
-      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
-      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
+      val cxT = ctyp_of thy xT
+      val cbodyT = ctyp_of thy bodyT
+      fun makeK () =
+        instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
+                     @{thm abs_K}
   in
       case body of
           Const _ => makeK()
@@ -145,7 +150,7 @@
   end;
 
 (* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
-fun do_introduce_combinators ct =
+fun introduce_combinators_in_cterm ct =
   if is_quasi_lambda_free (term_of ct) then
     Thm.reflexive ct
   else case term_of ct of
@@ -153,23 +158,23 @@
     let
       val (cv, cta) = Thm.dest_abs NONE ct
       val (v, _) = dest_Free (term_of cv)
-      val u_th = do_introduce_combinators cta
+      val u_th = introduce_combinators_in_cterm cta
       val cu = Thm.rhs_of u_th
       val comb_eq = abstract (Thm.cabs cv cu)
     in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   | _ $ _ =>
     let val (ct1, ct2) = Thm.dest_comb ct in
-        Thm.combination (do_introduce_combinators ct1)
-                        (do_introduce_combinators ct2)
+        Thm.combination (introduce_combinators_in_cterm ct1)
+                        (introduce_combinators_in_cterm ct2)
     end
 
-fun introduce_combinators th =
+fun introduce_combinators_in_theorem th =
   if is_quasi_lambda_free (prop_of th) then
     th
   else
     let
       val th = Drule.eta_contraction_rule th
-      val eqth = do_introduce_combinators (cprop_of th)
+      val eqth = introduce_combinators_in_cterm (cprop_of th)
     in Thm.equal_elim eqth th end
     handle THM (msg, _, _) =>
            (warning ("Error in the combinator translation of " ^
@@ -222,16 +227,17 @@
     |> Thm.varifyT_global
   end
 
-(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
+(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
+   into NNF. *)
 fun to_nnf th ctxt0 =
-  let val th1 = th |> transform_elim |> zero_var_indexes
+  let val th1 = th |> transform_elim_theorem |> zero_var_indexes
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
       val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
-                    |> extensionalize
+                    |> extensionalize_theorem
                     |> Meson.make_nnf ctxt
   in  (th3, ctxt)  end;
 
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+(* Skolemize a named theorem, with Skolem functions as additional premises. *)
 fun skolemize_theorem thy cheat th =
   let
     val ctxt0 = Variable.global_thm_context th
@@ -240,7 +246,7 @@
                       (assume_skolem_funs nnfth)
     val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
   in
-    cnfs |> map introduce_combinators
+    cnfs |> map introduce_combinators_in_theorem
          |> Variable.export ctxt ctxt0
          |> Meson.finish_cnf
          |> map Thm.close_derivation
@@ -255,6 +261,7 @@
 (**** Translate a set of theorems into CNF ****)
 
 (*The combination of rev and tail recursion preserves the original order*)
+(* ### FIXME: kill "cheat" *)
 fun cnf_rules_pairs thy cheat =
   let
     fun do_one _ [] = []
@@ -277,16 +284,7 @@
 val neg_clausify =
   single
   #> Meson.make_clauses_unsorted
-  #> map introduce_combinators
+  #> map introduce_combinators_in_theorem
   #> Meson.finish_cnf
 
-fun neg_conjecture_clauses ctxt st0 n =
-  let
-    (* "Option" is thrown if the assumptions contain schematic variables. *)
-    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
-    val ({params, prems, ...}, _) =
-      Subgoal.focus (Variable.set_body false ctxt) n st
-  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
-
-
 end;
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -34,6 +34,7 @@
                   literals: fol_literal list, ctypes_sorts: typ list}
 
   val type_wrapper_name : string
+  val bound_var_prefix : string
   val schematic_var_prefix: string
   val fixed_var_prefix: string
   val tvar_prefix: string
@@ -45,7 +46,8 @@
   val invert_const: string -> string
   val ascii_of: string -> string
   val undo_ascii_of: string -> string
-  val strip_prefix: string -> string -> string option
+  val strip_prefix_and_undo_ascii: string -> string -> string option
+  val make_bound_var : string -> string
   val make_schematic_var : string * int -> string
   val make_fixed_var : string -> string
   val make_schematic_type_var : string * int -> string
@@ -61,8 +63,10 @@
   val type_literals_for_types : typ list -> type_literal list
   val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
   val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
-  val type_of_combterm : combterm -> combtyp
+  val combtyp_of : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
+  val combterm_from_term :
+    theory -> (string * typ) list -> term -> combterm * typ list
   val literals_of_term : theory -> term -> fol_literal list * typ list
   val conceal_skolem_terms :
     int -> (string * term) list -> term -> (string * term) list * term
@@ -77,8 +81,9 @@
 
 val type_wrapper_name = "ti"
 
-val schematic_var_prefix = "V_";
-val fixed_var_prefix = "v_";
+val bound_var_prefix = "B_"
+val schematic_var_prefix = "V_"
+val fixed_var_prefix = "v_"
 
 val tvar_prefix = "T_";
 val tfree_prefix = "t_";
@@ -163,7 +168,7 @@
 
 (* If string s has the prefix s1, return the result of deleting it,
    un-ASCII'd. *)
-fun strip_prefix s1 s =
+fun strip_prefix_and_undo_ascii s1 s =
   if String.isPrefix s1 s then
     SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
   else
@@ -177,8 +182,9 @@
 fun ascii_of_indexname (v,0) = ascii_of v
   | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
 
-fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
-fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
+fun make_bound_var x = bound_var_prefix ^ ascii_of x
+fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
+fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
 
 fun make_schematic_type_var (x,i) =
       tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
@@ -373,9 +379,9 @@
 fun result_type (CombType (_, [_, tp2])) = tp2
   | result_type _ = raise Fail "non-function type"
 
-fun type_of_combterm (CombConst (_, tp, _)) = tp
-  | type_of_combterm (CombVar (_, tp)) = tp
-  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
+fun combtyp_of (CombConst (_, tp, _)) = tp
+  | combtyp_of (CombVar (_, tp)) = tp
+  | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
 
 (*gets the head of a combinator application, along with the list of arguments*)
 fun strip_combterm_comb u =
@@ -402,8 +408,13 @@
   | simp_type_of (TVar (x, _)) =
     CombTVar (make_schematic_type_var x, string_of_indexname x)
 
-(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of thy (Const (c, T)) =
+(* Converts a term (with combinators) into a combterm. Also accummulates sort
+   infomation. *)
+fun combterm_from_term thy bs (P $ Q) =
+      let val (P', tsP) = combterm_from_term thy bs P
+          val (Q', tsQ) = combterm_from_term thy bs Q
+      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
+  | combterm_from_term thy _ (Const (c, T)) =
       let
         val (tp, ts) = type_of T
         val tvar_list =
@@ -414,22 +425,25 @@
           |> map simp_type_of
         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
       in  (c',ts)  end
-  | combterm_of _ (Free(v, T)) =
+  | combterm_from_term _ _ (Free (v, T)) =
       let val (tp,ts) = type_of T
           val v' = CombConst (`make_fixed_var v, tp, [])
       in  (v',ts)  end
-  | combterm_of _ (Var(v, T)) =
+  | combterm_from_term _ _ (Var (v, T)) =
       let val (tp,ts) = type_of T
           val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
       in  (v',ts)  end
-  | combterm_of thy (P $ Q) =
-      let val (P', tsP) = combterm_of thy P
-          val (Q', tsQ) = combterm_of thy Q
-      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
-  | combterm_of _ (Abs _) = raise Fail "HOL clause: Abs"
+  | combterm_from_term _ bs (Bound j) =
+      let
+        val (s, T) = nth bs j
+        val (tp, ts) = type_of T
+        val v' = CombConst (`make_bound_var s, tp, [])
+      in (v', ts) end
+  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
-  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
+  | predicate_of thy (t, pos) =
+    (combterm_from_term thy [] (Envir.eta_contract t), pos)
 
 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
     literals_of_term1 args thy P
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -100,7 +100,7 @@
       wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
-                  type_of_combterm tm);
+                  combtyp_of tm)
 
 fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
@@ -223,15 +223,15 @@
 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
 
 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
-     (case strip_prefix tvar_prefix v of
+     (case strip_prefix_and_undo_ascii tvar_prefix v of
           SOME w => make_tvar w
         | NONE   => make_tvar v)
   | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
-     (case strip_prefix type_const_prefix x of
+     (case strip_prefix_and_undo_ascii type_const_prefix x of
           SOME tc => Term.Type (invert_const tc,
                                 map (hol_type_from_metis_term ctxt) tys)
         | NONE    =>
-      case strip_prefix tfree_prefix x of
+      case strip_prefix_and_undo_ascii tfree_prefix x of
           SOME tf => mk_tfree ctxt tf
         | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
 
@@ -241,10 +241,10 @@
       val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
                                   Metis.Term.toString fol_tm)
       fun tm_to_tt (Metis.Term.Var v) =
-             (case strip_prefix tvar_prefix v of
+             (case strip_prefix_and_undo_ascii tvar_prefix v of
                   SOME w => Type (make_tvar w)
                 | NONE =>
-              case strip_prefix schematic_var_prefix v of
+              case strip_prefix_and_undo_ascii schematic_var_prefix v of
                   SOME w => Term (mk_var (w, HOLogic.typeT))
                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
                     (*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -261,7 +261,7 @@
       and applic_to_tt ("=",ts) =
             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
         | applic_to_tt (a,ts) =
-            case strip_prefix const_prefix a of
+            case strip_prefix_and_undo_ascii const_prefix a of
                 SOME b =>
                   let val c = invert_const b
                       val ntypes = num_type_args thy c
@@ -279,14 +279,14 @@
                                    cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
                      end
               | NONE => (*Not a constant. Is it a type constructor?*)
-            case strip_prefix type_const_prefix a of
+            case strip_prefix_and_undo_ascii type_const_prefix a of
                 SOME b =>
                   Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
-            case strip_prefix tfree_prefix a of
+            case strip_prefix_and_undo_ascii tfree_prefix a of
                 SOME b => Type (mk_tfree ctxt b)
               | NONE => (*a fixed variable? They are Skolem functions.*)
-            case strip_prefix fixed_var_prefix a of
+            case strip_prefix_and_undo_ascii fixed_var_prefix a of
                 SOME b =>
                   let val opr = Term.Free(b, HOLogic.typeT)
                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
@@ -302,16 +302,16 @@
   let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
                                   Metis.Term.toString fol_tm)
       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
-             (case strip_prefix schematic_var_prefix v of
+             (case strip_prefix_and_undo_ascii schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
             Const ("op =", HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
-           (case strip_prefix const_prefix x of
+           (case strip_prefix_and_undo_ascii const_prefix x of
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
-            case strip_prefix fixed_var_prefix x of
+            case strip_prefix_and_undo_ascii fixed_var_prefix x of
                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
               | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -322,10 +322,10 @@
         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis.Term.Fn (x, [])) =
-           (case strip_prefix const_prefix x of
+           (case strip_prefix_and_undo_ascii const_prefix x of
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
-            case strip_prefix fixed_var_prefix x of
+            case strip_prefix_and_undo_ascii fixed_var_prefix x of
                 SOME v => Free (v, dummyT)
               | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
                   hol_term_from_metis_PT ctxt t))
@@ -405,9 +405,9 @@
                                        " in " ^ Display.string_of_thm ctxt i_th);
                  NONE)
       fun remove_typeinst (a, t) =
-            case strip_prefix schematic_var_prefix a of
+            case strip_prefix_and_undo_ascii schematic_var_prefix a of
                 SOME b => SOME (b, t)
-              | NONE   => case strip_prefix tvar_prefix a of
+              | NONE   => case strip_prefix_and_undo_ascii tvar_prefix a of
                 SOME _ => NONE          (*type instantiations are forbidden!*)
               | NONE   => SOME (a,t)    (*internal Metis var?*)
       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -16,7 +16,8 @@
     Proof.context -> thm list -> Facts.ref -> string * thm list
   val relevant_facts :
     bool -> real -> real -> bool -> int -> bool -> relevance_override
-    -> Proof.context * (thm list * 'a) -> thm list -> (string * thm) list
+    -> Proof.context * (thm list * 'a) -> term list -> term
+    -> (string * thm) list
 end;
 
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -148,9 +149,8 @@
         do_term t0 #> do_formula pos t1  (* theory constant *)
       | _ => do_term t
   in
-    Symtab.empty
-    |> fold (Symtab.update o rpair []) boring_natural_consts
-    |> fold (do_formula pos) ts
+    Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
+                 |> fold (do_formula pos) ts
   end
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
@@ -343,7 +343,7 @@
 
 fun relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
-                     thy axioms goals =
+                     thy axioms goal_ts =
   if relevance_threshold > 1.0 then
     []
   else if relevance_threshold < 0.0 then
@@ -352,7 +352,7 @@
     let
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
-      val goal_const_tab = get_consts_typs thy (SOME true) goals
+      val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
       val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
       val _ =
         trace_msg (fn () => "Initial constants: " ^
@@ -563,12 +563,14 @@
 fun relevant_facts full_types relevance_threshold relevance_convergence
                    defs_relevant max_new theory_relevant
                    (relevance_override as {add, del, only})
-                   (ctxt, (chained_ths, _)) goal_cls =
+                   (ctxt, (chained_ths, _)) hyp_ts concl_t =
   let
     val thy = ProofContext.theory_of ctxt
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val has_override = not (null add) orelse not (null del)
-    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
+(*###
+    val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts)
+*)
     val axioms =
       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
           (map (name_thms_pair_from_ref ctxt chained_ths) add @
@@ -581,7 +583,7 @@
   in
     relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
-                     thy axioms (map prop_of goal_cls)
+                     thy axioms (concl_t :: hyp_ts)
     |> has_override ? make_unique
     |> sort_wrt fst
   end
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -55,13 +55,12 @@
     val _ = priority ("Testing " ^ string_of_int num_theorems ^
                       " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
-    val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_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 axclauses,
-      filtered_clauses = SOME (the_default axclauses filtered_clauses)}
+      axiom_clauses = SOME name_thm_pairs,
+      filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
   in
     prover params (K "") timeout problem
     |> tap (fn result : prover_result =>
@@ -126,8 +125,7 @@
                \option (e.g., \"timeout = " ^
                string_of_int (10 + msecs div 1000) ^ " s\").")
     | {message, ...} => (NONE, "ATP error: " ^ message))
-    handle TRIVIAL () => (SOME [], metis_line full_types i n [])
-         | ERROR msg => (NONE, "Error: " ^ msg)
+    handle ERROR msg => (NONE, "Error: " ^ msg)
   end
 
 end;
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -14,11 +14,11 @@
     bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val isar_proof_text:
-    string Symtab.table * bool * int * Proof.context * int list list
+    string Symtab.table * bool * int * Proof.context * int list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val proof_text:
-    bool -> string Symtab.table * bool * int * Proof.context * int list list
+    bool -> string Symtab.table * bool * int * Proof.context * int list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
 end;
@@ -33,22 +33,28 @@
 
 type minimize_command = string list -> string
 
-val index_in_shape : int -> int list list -> int =
-  find_index o exists o curry (op =)
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
+
+val index_in_shape : int -> int list -> int = find_index o curry (op =)
 fun is_axiom_clause_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 =
   index_in_shape num conjecture_shape >= 0
 
-fun smart_lambda v t =
-  Abs (case v of
-         Const (s, _) =>
-         List.last (space_explode skolem_infix (Long_Name.base_name s))
-       | Var ((s, _), _) => s
-       | Free (s, _) => s
-       | _ => "", fastype_of v, abstract_over (v, t))
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
+fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
+  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
+  | negate_term (@{const "op -->"} $ t1 $ t2) =
+    @{const "op &"} $ t1 $ negate_term t2
+  | negate_term (@{const "op &"} $ t1 $ t2) =
+    @{const "op |"} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const "op |"} $ t1 $ t2) =
+    @{const "op &"} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const Not} $ t) = t
+  | negate_term t = @{const Not} $ t
 
 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
   Definition of 'a * 'b * 'c |
@@ -56,86 +62,92 @@
 
 (**** PARSING OF TSTP FORMAT ****)
 
-(* Syntax trees, either term list or formulae *)
-datatype node = IntLeaf of int | StrNode of string * node list
-
-fun str_leaf s = StrNode (s, [])
-
-fun scons (x, y) = StrNode ("cons", [x, y])
-val slist_of = List.foldl scons (str_leaf "nil")
+datatype int_or_string = Str of string | Int of int
 
 (*Strings enclosed in single quotes, e.g. filenames*)
-val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
+val scan_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
 
-val parse_dollar_name =
+val scan_dollar_name =
   Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
 
 (* needed for SPASS's output format *)
 fun repair_name _ "$true" = "c_True"
   | repair_name _ "$false" = "c_False"
-  | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
+  | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
   | repair_name _ "equal" = "c_equal" (* probably not needed *)
   | repair_name pool s = Symtab.lookup pool s |> the_default s
 (* Generalized first-order terms, which include file names, numbers, etc. *)
 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    forever at compile time. *)
+fun parse_generalized_term x =
+  (scan_quoted >> (fn s => ATerm (Str s, []))
+   || scan_dollar_name
+      -- Scan.optional ($$ "(" |-- parse_generalized_terms --| $$ ")") []
+      >> (fn (s, gs) => ATerm (Str s, gs))
+   || scan_integer >> (fn k => ATerm (Int k, []))
+   || $$ "(" |-- parse_generalized_term --| $$ ")"
+   || $$ "[" |-- Scan.optional parse_generalized_terms [] --| $$ "]"
+      >> curry ATerm (Str "list")) x
+and parse_generalized_terms x =
+  (parse_generalized_term ::: Scan.repeat ($$ "," |-- parse_generalized_term)) x
 fun parse_term pool x =
-     (parse_quoted >> str_leaf
-   || scan_integer >> IntLeaf
-   || (parse_dollar_name >> repair_name pool)
-      -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
-   || $$ "(" |-- parse_term pool --| $$ ")"
-   || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
+  ((scan_dollar_name >> repair_name pool)
+    -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> ATerm) x
 and parse_terms pool x =
   (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
 
-fun negate_node u = StrNode ("c_Not", [u])
-fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
-
-(* Apply equal or not-equal to a term. *)
-fun repair_predicate_term (u, NONE) = u
-  | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
-  | repair_predicate_term (u1, SOME (SOME _, u2)) =
-    negate_node (equate_nodes u1 u2)
 fun parse_predicate_term pool =
   parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
                                   -- parse_term pool)
-  >> repair_predicate_term
-fun parse_literal pool x =
-  ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
-fun parse_literals pool =
-  parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
-fun parse_parenthesized_literals pool =
-  $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
-fun parse_clause pool =
-  parse_parenthesized_literals pool
-    ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
-  >> List.concat
+  >> (fn (u, NONE) => APred u
+       | (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2]))
+       | (u1, SOME (SOME _, u2)) =>
+         mk_anot (APred (ATerm ("c_equal", [u1, u2]))))
+
+fun fo_term_head (ATerm (s, _)) = s
 
-fun ints_of_node (IntLeaf n) = cons n
-  | ints_of_node (StrNode (_, us)) = fold ints_of_node us
+(* TPTP formulas are fully parenthesized, so we don't need to worry about
+   operator precedence. *)
+fun parse_formula pool x =
+  (($$ "(" |-- parse_formula pool --| $$ ")"
+    || ($$ "!" >> K AForall || $$ "?" >> K AExists)
+       --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
+       -- parse_formula pool
+       >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
+    || $$ "~" |-- parse_formula pool >> mk_anot
+    || parse_predicate_term pool)
+   -- Scan.option ((Scan.this_string "=>" >> K AImplies
+                    || Scan.this_string "<=>" >> K AIff
+                    || Scan.this_string "<~>" >> K ANotIff
+                    || Scan.this_string "<=" >> K AIf
+                    || $$ "|" >> K AOr || $$ "&" >> K AAnd)
+                   -- parse_formula pool)
+   >> (fn (phi1, NONE) => phi1
+        | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
+
+fun ints_of_generalized_term (ATerm (label, gs)) =
+  fold ints_of_generalized_term gs #> (case label of Int k => cons k | _ => I)
 val parse_tstp_annotations =
-  Scan.optional ($$ "," |-- parse_term Symtab.empty
-                   --| Scan.option ($$ "," |-- parse_terms Symtab.empty)
-                 >> (fn source => ints_of_node source [])) []
+  Scan.optional ($$ "," |-- parse_generalized_term
+                   --| Scan.option ($$ "," |-- parse_generalized_terms)
+                 >> (fn g => ints_of_generalized_term g [])) []
 
-fun parse_definition pool =
-  $$ "(" |-- parse_literal pool --| Scan.this_string "<=>"
-  -- parse_clause pool --| $$ ")"
-
-(* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
+(* Syntax: (fof|cnf)\(<num>, <formula_role>, <cnf_formula> <annotations>\).
    The <num> could be an identifier, but we assume integers. *)
-fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
-fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
-fun parse_tstp_line pool =
-     ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ ","
-       --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
-       --| parse_tstp_annotations --| $$ ")" --| $$ "."
-      >> finish_tstp_definition_line)
-  || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ ","
-       --| Symbol.scan_id --| $$ "," -- parse_clause pool
-       -- parse_tstp_annotations --| $$ ")" --| $$ "."
-      >> finish_tstp_inference_line)
+ fun parse_tstp_line pool =
+   ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
+     |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ","
+     -- parse_formula pool -- parse_tstp_annotations --| $$ ")" --| $$ "."
+    >> (fn (((num, role), phi), deps) =>
+           case role of
+             "definition" =>
+             (case phi of
+                AConn (AIff, [phi1 as APred _, phi2]) =>
+                Definition (num, phi1, phi2)
+              | APred (ATerm ("$$e", _)) =>
+                Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
+              | _ => raise Fail "malformed definition")
+           | _ => Inference (num, phi, deps))
 
 (**** PARSING OF SPASS OUTPUT ****)
 
@@ -152,21 +164,25 @@
 fun parse_decorated_predicate_term pool =
   parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
 
+fun mk_horn ([], []) = APred (ATerm ("c_False", []))
+  | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
+  | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
+  | mk_horn (neg_lits, pos_lits) =
+    mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
+                       foldr1 (mk_aconn AOr) pos_lits)
+
 fun parse_horn_clause pool =
   Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
     -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
     -- Scan.repeat (parse_decorated_predicate_term pool)
-  >> (fn (([], []), []) => [str_leaf "c_False"]
-       | ((clauses1, clauses2), clauses3) =>
-         map negate_node (clauses1 @ clauses2) @ clauses3)
+  >> (mk_horn o apfst (op @))
 
 (* Syntax: <num>[0:<inference><annotations>]
    <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
-fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
 fun parse_spass_line pool =
   scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
-  >> finish_spass_line
+  >> (fn ((num, deps), u) => Inference (num, u, deps))
 
 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
 fun parse_lines pool = Scan.repeat1 (parse_line pool)
@@ -178,30 +194,31 @@
 
 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
 
-exception NODE of node list
+exception FO_TERM of string fo_term list
+exception FORMULA of (string, string fo_term) formula list
+exception SAME of unit
 
 (* Type variables are given the basic sort "HOL.type". Some will later be
-  constrained by information from type literals, or by type inference. *)
-fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
-  | type_from_node tfrees (u as StrNode (a, us)) =
-    let val Ts = map (type_from_node tfrees) us in
-      case strip_prefix type_const_prefix a of
-        SOME b => Type (invert_const b, Ts)
+   constrained by information from type literals, or by type inference. *)
+fun type_from_fo_term tfrees (u as ATerm (a, us)) =
+  let val Ts = map (type_from_fo_term tfrees) us in
+    case strip_prefix_and_undo_ascii type_const_prefix a of
+      SOME b => Type (invert_const b, Ts)
+    | NONE =>
+      if not (null us) then
+        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
+      else case strip_prefix_and_undo_ascii tfree_prefix a of
+        SOME b =>
+        let val s = "'" ^ b in
+          TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+        end
       | NONE =>
-        if not (null us) then
-          raise NODE [u]  (* only "tconst"s have type arguments *)
-        else case strip_prefix tfree_prefix a of
-          SOME b =>
-          let val s = "'" ^ b in
-            TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
-          end
+        case strip_prefix_and_undo_ascii tvar_prefix a of
+          SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
         | NONE =>
-          case strip_prefix tvar_prefix a of
-            SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
-          | NONE =>
-            (* Variable from the ATP, say "X1" *)
-            Type_Infer.param 0 (a, HOLogic.typeS)
-    end
+          (* Variable from the ATP, say "X1" *)
+          Type_Infer.param 0 (a, HOLogic.typeS)
+  end
 
 fun fix_atp_variable_name s =
   let
@@ -222,21 +239,19 @@
 
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred.*)
-fun term_from_node thy full_types tfrees =
+fun term_from_fo_term thy full_types tfrees opt_T =
   let
     fun aux opt_T extra_us u =
       case u of
-        IntLeaf _ => raise NODE [u]
-      | StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
-      | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
-      | StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1
-      | StrNode (a, us) =>
+        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
+      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
+      | ATerm (a, us) =>
         if a = type_wrapper_name then
           case us of
             [typ_u, term_u] =>
-            aux (SOME (type_from_node tfrees typ_u)) extra_us term_u
-          | _ => raise NODE us
-        else case strip_prefix const_prefix a of
+            aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
+          | _ => raise FO_TERM us
+        else case strip_prefix_and_undo_ascii const_prefix a of
           SOME "equal" =>
           list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
                      map (aux NONE []) us)
@@ -260,39 +275,35 @@
                             else
                               raise Fail ("no type information for " ^ quote c)
                         else
-                          if String.isPrefix skolem_theory_name c then
-                            map fastype_of term_ts ---> HOLogic.typeT
-                          else
-                            Sign.const_instance thy (c,
-                                map (type_from_node tfrees) type_us))
+                          Sign.const_instance thy (c,
+                              map (type_from_fo_term tfrees) type_us))
           in list_comb (t, term_ts @ extra_ts) end
         | NONE => (* a free or schematic variable *)
           let
             val ts = map (aux NONE []) (us @ extra_us)
             val T = map fastype_of ts ---> HOLogic.typeT
             val t =
-              case strip_prefix fixed_var_prefix a of
+              case strip_prefix_and_undo_ascii fixed_var_prefix a of
                 SOME b => Free (b, T)
               | NONE =>
-                case strip_prefix schematic_var_prefix a of
+                case strip_prefix_and_undo_ascii schematic_var_prefix a of
                   SOME b => Var ((b, 0), T)
                 | NONE =>
                   (* Variable from the ATP, say "X1" *)
                   Var ((fix_atp_variable_name a, 0), T)
           in list_comb (t, ts) end
-  in aux end
+  in aux opt_T [] end
 
 (* Type class literal applied to a type. Returns triple of polarity, class,
    type. *)
-fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
-    type_constraint_from_node (not pos) tfrees u
-  | type_constraint_from_node pos tfrees u = case u of
-        IntLeaf _ => raise NODE [u]
-      | StrNode (a, us) =>
-            (case (strip_prefix class_prefix a,
-                   map (type_from_node tfrees) us) of
-                 (SOME b, [T]) => (pos, b, T)
-               | _ => raise NODE [u])
+fun type_constraint_from_formula pos tfrees (AConn (ANot, [u])) =
+    type_constraint_from_formula (not pos) tfrees u
+  | type_constraint_from_formula pos tfrees (phi as APred (ATerm (a, us))) =
+    (case (strip_prefix_and_undo_ascii class_prefix a,
+           map (type_from_fo_term tfrees) us) of
+       (SOME b, [T]) => (pos, b, T)
+     | _ => raise FORMULA [phi])
+  | type_constraint_from_formula _ _ phi = raise FORMULA [phi]
 
 (** Accumulate type constraints in a clause: negative type literals **)
 
@@ -305,68 +316,6 @@
 fun is_positive_literal (@{const Not} $ _) = false
   | is_positive_literal _ = true
 
-fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
-    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
-  | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
-    Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
-  | negate_term thy (@{const "op -->"} $ t1 $ t2) =
-    @{const "op &"} $ t1 $ negate_term thy t2
-  | negate_term thy (@{const "op &"} $ t1 $ t2) =
-    @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
-  | negate_term thy (@{const "op |"} $ t1 $ t2) =
-    @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
-  | negate_term _ (@{const Not} $ t) = t
-  | negate_term _ t = @{const Not} $ t
-
-fun clause_for_literals _ [] = HOLogic.false_const
-  | clause_for_literals _ [lit] = lit
-  | clause_for_literals thy lits =
-    case List.partition is_positive_literal lits of
-      (pos_lits as _ :: _, neg_lits as _ :: _) =>
-      @{const "op -->"}
-          $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
-          $ foldr1 HOLogic.mk_disj pos_lits
-    | _ => foldr1 HOLogic.mk_disj lits
-
-(* Final treatment of the list of "real" literals from a clause.
-   No "real" literals means only type information. *)
-fun finish_clause _ [] = HOLogic.true_const
-  | finish_clause thy lits =
-    lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
-         |> clause_for_literals thy
-
-(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_nodes thy full_types tfrees =
-  let
-    fun aux (vt, lits) [] = (vt, finish_clause thy lits)
-      | aux (vt, lits) (u :: us) =
-        aux (add_type_constraint
-                 (type_constraint_from_node true tfrees u) vt, lits) us
-        handle NODE _ =>
-               aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
-                                       [] u :: lits) us
-  in aux end
-
-(* Update TVars with detected sort constraints. It's not totally clear when
-   this code is necessary. *)
-fun repair_tvar_sorts vt =
-  let
-    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
-      | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
-      | do_type (TFree z) = TFree z
-    fun do_term (Const (a, T)) = Const (a, do_type T)
-      | do_term (Free (a, T)) = Free (a, do_type T)
-      | do_term (Var (xi, T)) = Var (xi, do_type T)
-      | do_term (t as Bound _) = t
-      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
-      | do_term (t1 $ t2) = do_term t1 $ do_term t2
-  in not (Vartab.is_empty vt) ? do_term end
-
-fun unskolemize_term t =
-  Term.add_consts t []
-  |> filter (is_skolem_const_name o fst) |> map Const
-  |> rpair t |-> fold forall_of
-
 val combinator_table =
   [(@{const_name COMBI}, @{thm COMBI_def_raw}),
    (@{const_name COMBK}, @{thm COMBK_def_raw}),
@@ -382,14 +331,75 @@
      | NONE => t)
   | uncombine_term t = t
 
-(* Interpret a list of syntax trees as a clause, given by "real" literals and
-   sort constraints. "vt" holds the initial sort constraints, from the
-   conjecture clauses. *)
-fun clause_of_nodes ctxt full_types tfrees us =
+fun disjuncts (AConn (AOr, phis)) = maps disjuncts phis
+  | disjuncts phi = [phi]
+
+(* Update schematic type variables with detected sort constraints. It's not
+   totally clear when this code is necessary. *)
+fun repair_tvar_sorts (tvar_tab, t) =
   let
-    val thy = ProofContext.theory_of ctxt
-    val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
-  in repair_tvar_sorts vt t end
+    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+      | do_type (TVar (xi, s)) =
+        TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
+      | do_type (TFree z) = TFree z
+    fun do_term (Const (a, T)) = Const (a, do_type T)
+      | do_term (Free (a, T)) = Free (a, do_type T)
+      | do_term (Var (xi, T)) = Var (xi, do_type T)
+      | do_term (t as Bound _) = t
+      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+      | do_term (t1 $ t2) = do_term t1 $ do_term t2
+  in t |> not (Vartab.is_empty tvar_tab) ? do_term end
+
+fun s_disj (t1, @{const False}) = t1
+  | s_disj p = HOLogic.mk_disj p
+
+fun quantify_over_free quant_s free_s body_t =
+  case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of
+    [] => body_t
+  | 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, given by "real" literals and
+   sort constraints. Accumulates sort constraints in "tvar_tab", with "real"
+   literals in "lits". *)
+fun prop_from_formula thy full_types tfrees =
+   let
+    val do_sort_constraint =
+      add_type_constraint o type_constraint_from_formula true tfrees
+    fun do_real_literal phi =
+      case phi of
+        AQuant (_, [], phi) => do_real_literal phi
+      | AQuant (q, x :: xs, phi') =>
+        let
+          val body = do_real_literal (AQuant (q, xs, phi'))
+          val quant_s = case q of
+                          AForall => @{const_name All}
+                        | AExists => @{const_name Ex}
+        in quantify_over_free quant_s x body end
+      | AConn (ANot, [phi']) => HOLogic.mk_not (do_real_literal phi')
+      | AConn (c, [phi1, phi2]) =>
+        (phi1, phi2)
+        |> pairself do_real_literal
+        |> (case c of
+              AAnd => HOLogic.mk_conj
+            | AOr => HOLogic.mk_disj
+            | AImplies => HOLogic.mk_imp
+            | AIff => (fn (t1, t2) => HOLogic.eq_const HOLogic.boolT $ t1 $ t2))
+      | APred tm =>
+        term_from_fo_term thy full_types tfrees (SOME @{typ bool}) tm
+      | _ => raise FORMULA [phi]
+    fun do_literals (tvar_tab, t) [] = (tvar_tab, t)
+      | do_literals (tvar_tab, t) (u :: us) =
+        (do_literals (tvar_tab |> do_sort_constraint u, t) us
+         handle FO_TERM _ => raise SAME ()
+              | FORMULA _ => raise SAME ())
+        handle SAME () =>
+               do_literals (tvar_tab, s_disj (do_real_literal u, t)) us
+  in
+    repair_tvar_sorts o do_literals (Vartab.empty, HOLogic.false_const)
+    o disjuncts
+  end
+
 fun check_formula ctxt =
   Type_Infer.constrain @{typ bool}
   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
@@ -400,13 +410,14 @@
 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
 
-fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
+fun decode_line full_types tfrees (Definition (num, phi1, phi2)) ctxt =
     let
-      val t1 = clause_of_nodes ctxt full_types tfrees [u]
+      val thy = ProofContext.theory_of ctxt
+      val t1 = prop_from_formula thy full_types tfrees phi1
       val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = clause_of_nodes ctxt full_types tfrees us
+      val t2 = prop_from_formula thy full_types tfrees phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> uncombine_term |> check_formula ctxt
@@ -415,10 +426,11 @@
       (Definition (num, t1, t2),
        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
-  | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
+  | decode_line full_types tfrees (Inference (num, u, deps)) ctxt =
     let
-      val t = us |> clause_of_nodes ctxt full_types tfrees
-                 |> unskolemize_term |> uncombine_term |> check_formula ctxt
+      val thy = ProofContext.theory_of ctxt
+      val t = u |> prop_from_formula thy full_types tfrees
+                |> uncombine_term |> check_formula ctxt
     in
       (Inference (num, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
@@ -507,11 +519,10 @@
 
 (** EXTRACTING LEMMAS **)
 
-(* A list consisting of the first number in each line is returned.
-   TSTP: Interesting lines have the form "fof(108, axiom, ...)", where the
-   number (108) is extracted.
-   SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
-   extracted. *)
+(* A list consisting of the first number in each line is returned. For TSTP,
+   interesting lines have the form "fof(108, axiom, ...)", where the number
+   (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
+   the first number (108) is extracted. *)
 fun extract_formula_numbers_in_atp_proof atp_proof =
   let
     val tokens_of = String.tokens (not o Char.isAlphaNum)
@@ -600,6 +611,7 @@
   else
     apfst (insert (op =) (raw_prefix, num))
 
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
 
 fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
@@ -613,7 +625,7 @@
                          atp_proof conjecture_shape thm_names params frees =
   let
     val lines =
-      atp_proof ^ "$" (* the $ sign acts as a sentinel *)
+      atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: pick it up) *)
       |> parse_proof pool
       |> decode_lines ctxt full_types tfrees
       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
@@ -674,32 +686,26 @@
   | 1 => [Then]
   | _ => [Ultimately]
 
-fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
+fun redirect_proof conjecture_shape hyp_ts concl_t proof =
   let
     (* The first pass outputs those steps that are independent of the negated
        conjecture. The second pass flips the proof by contradiction to obtain a
        direct proof, introducing case splits when an inference depends on
        several facts that depend on the negated conjecture. *)
     fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
-    val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
-    val canonicalize_labels =
-      map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
-      #> distinct (op =)
+    val concl_l = (raw_prefix, List.last conjecture_shape)
     fun first_pass ([], contra) = ([], contra)
       | first_pass ((step as Fix _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
       | first_pass ((step as Let _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
       | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
-        if member (op =) concl_ls l then
-          first_pass (proof, contra ||> l = hd concl_ls ? cons step)
+        if l = concl_l then
+          first_pass (proof, contra ||> l = concl_l ? cons step)
         else
           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
-        let
-          val ls = canonicalize_labels ls
-          val step = Have (qs, l, t, ByMetis (ls, ss))
-        in
+        let val step = Have (qs, l, t, ByMetis (ls, ss)) in
           if exists (member (op =) (fst contra)) ls then
             first_pass (proof, contra |>> cons l ||> cons step)
           else
@@ -707,7 +713,7 @@
         end
       | first_pass _ = raise Fail "malformed proof"
     val (proof_top, (contra_ls, contra_proof)) =
-      first_pass (proof, (concl_ls, []))
+      first_pass (proof, ([concl_l], []))
     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
     fun backpatch_labels patches ls =
       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
@@ -733,16 +739,16 @@
                            (proof, assums,
                             patches |>> cons (contra_l, (l :: co_ls, ss)))
                |>> cons (if member (op =) (fst (snd patches)) l then
-                           Assume (l, negate_term thy t)
+                           Assume (l, negate_term t)
                          else
-                           Have (qs, l, negate_term thy t,
+                           Have (qs, l, negate_term t,
                                  ByMetis (backpatch_label patches l)))
            | (contra_ls as _ :: _, co_ls) =>
              let
                val proofs =
                  map_filter
                      (fn l =>
-                         if member (op =) concl_ls l then
+                         if l = concl_l then
                            NONE
                          else
                            let
@@ -756,7 +762,7 @@
                            end) contra_ls
                val (assumes, facts) =
                  if member (op =) (fst (snd patches)) l then
-                   ([Assume (l, negate_term thy t)], (l :: co_ls, ss))
+                   ([Assume (l, negate_term t)], (l :: co_ls, ss))
                  else
                    ([], (co_ls, ss))
              in
@@ -927,18 +933,12 @@
         do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   in do_proof end
 
-fun strip_subgoal goal i =
-  let
-    val (t, frees) = Logic.goal_params (prop_of goal) i
-    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
-    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
-  in (rev (map dest_Free frees), hyp_ts, concl_t) end
-
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
                     (other_params as (full_types, _, atp_proof, thm_names, goal,
                                       i)) =
   let
-    val thy = ProofContext.theory_of ctxt
+    (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal
+       to ATP_Systems *)
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
@@ -948,7 +948,7 @@
       case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
                                 atp_proof conjecture_shape thm_names params
                                 frees
-           |> redirect_proof thy conjecture_shape hyp_ts concl_t
+           |> redirect_proof conjecture_shape hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof
            |> then_chain_proof
            |> kill_useless_labels_in_proof
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -7,14 +7,31 @@
 
 signature SLEDGEHAMMER_TPTP_FORMAT =
 sig
+  type name = Metis_Clauses.name
+  type kind = Metis_Clauses.kind
+  type combterm = Metis_Clauses.combterm
   type class_rel_clause = Metis_Clauses.class_rel_clause
   type arity_clause = Metis_Clauses.arity_clause
-  type fol_clause = Metis_Clauses.fol_clause
+
+  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+  datatype quantifier = AForall | AExists
+  datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+  datatype ('a, 'b) formula =
+    AQuant of quantifier * 'a list * ('a, 'b) formula |
+    AConn of connective * ('a, 'b) formula list |
+    APred of 'b
+
+  datatype fol_formula =
+    FOLFormula of {formula_name: string,
+                   kind: kind,
+                   combformula: (name, combterm) formula,
+                   ctypes_sorts: typ list}
 
   val axiom_prefix : string
+  val conjecture_prefix : string
   val write_tptp_file :
-    theory -> bool -> bool -> bool -> Path.T
-    -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
+    theory -> bool -> bool -> bool -> bool -> Path.T
+    -> fol_formula list * fol_formula list * fol_formula list * fol_formula list
        * class_rel_clause list * arity_clause list
     -> string Symtab.table * int
 end;
@@ -30,15 +47,19 @@
 
 datatype 'a fo_term = ATerm of 'a * 'a fo_term list
 datatype quantifier = AForall | AExists
-datatype connective = ANot | AAnd | AOr | AImplies | AIff
-datatype 'a formula =
-  AQuant of quantifier * 'a list * 'a formula |
-  AConn of connective * 'a formula list |
-  APred of 'a fo_term
+datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+datatype ('a, 'b) formula =
+  AQuant of quantifier * 'a list * ('a, 'b) formula |
+  AConn of connective * ('a, 'b) formula list |
+  APred of 'b
 
 fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_ahorn [] phi = phi
+  | mk_ahorn (phi :: phis) psi =
+    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
 
-datatype 'a problem_line = Fof of string * kind * 'a formula
+datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
 type 'a problem = (string * 'a problem_line list) list
 
 fun string_for_term (ATerm (s, [])) = s
@@ -51,10 +72,14 @@
   | string_for_connective AAnd = "&"
   | string_for_connective AOr = "|"
   | string_for_connective AImplies = "=>"
+  | string_for_connective AIf = "<="
   | string_for_connective AIff = "<=>"
+  | string_for_connective ANotIff = "<~>"
 fun string_for_formula (AQuant (q, xs, phi)) =
-    string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
+    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
     string_for_formula phi
+  | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
+    space_implode " != " (map string_for_term ts)
   | string_for_formula (AConn (c, [phi])) =
     string_for_connective c ^ " " ^ string_for_formula phi
   | string_for_formula (AConn (c, phis)) =
@@ -137,11 +162,16 @@
 
 (** Sledgehammer stuff **)
 
+datatype fol_formula =
+  FOLFormula of {formula_name: string,
+                 kind: kind,
+                 combformula: (name, combterm) formula,
+                 ctypes_sorts: typ list}
+
 val axiom_prefix = "ax_"
 val conjecture_prefix = "conj_"
 val arity_clause_prefix = "clsarity_"
-
-fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name
+val tfrees_name = "tfrees"
 
 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
 
@@ -150,49 +180,51 @@
   | fo_term_for_combtyp (CombType (name, tys)) =
     ATerm (name, map fo_term_for_combtyp tys)
 
-fun fo_term_for_combterm full_types top_level u =
-  let
-    val (head, args) = strip_combterm_comb u
-    val (x, ty_args) =
-      case head of
-        CombConst (name, _, ty_args) =>
-        if fst name = "equal" then
-          (if top_level andalso length args = 2 then name
-           else ("c_fequal", @{const_name fequal}), [])
-        else
-          (name, if full_types then [] else ty_args)
-      | CombVar (name, _) => (name, [])
-      | CombApp _ => raise Fail "impossible \"CombApp\""
-    val t = ATerm (x, map fo_term_for_combtyp ty_args @
-                      map (fo_term_for_combterm full_types false) args)
-  in
-    if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t
-    else t
-  end
-
-fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) =
-  (pos, fo_term_for_combterm full_types true t)
-
-fun fo_literal_for_type_literal pos (TyLitVar (class, name)) =
-    (pos, ATerm (class, [ATerm (name, [])]))
-  | fo_literal_for_type_literal pos (TyLitFree (class, name)) =
-    (pos, ATerm (class, [ATerm (name, [])]))
+fun fo_literal_for_type_literal (TyLitVar (class, name)) =
+    (true, ATerm (class, [ATerm (name, [])]))
+  | fo_literal_for_type_literal (TyLitFree (class, name)) =
+    (true, ATerm (class, [ATerm (name, [])]))
 
 fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
-fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), []))
-  | formula_for_fo_literals (lit :: lits) =
-    AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits])
 
-fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) =
-  map (fo_literal_for_literal full_types) literals @
-  map (fo_literal_for_type_literal false)
-      (type_literals_for_types ctypes_sorts)
-  |> formula_for_fo_literals
+fun fo_term_for_combterm full_types =
+  let
+    fun aux top_level u =
+      let
+        val (head, args) = strip_combterm_comb u
+        val (x, ty_args) =
+          case head of
+            CombConst (name, _, ty_args) =>
+            if fst name = "equal" then
+              (if top_level andalso length args = 2 then name
+               else ("c_fequal", @{const_name fequal}), [])
+            else
+              (name, if full_types then [] else ty_args)
+          | CombVar (name, _) => (name, [])
+          | CombApp _ => raise Fail "impossible \"CombApp\""
+        val t = ATerm (x, map fo_term_for_combtyp ty_args @
+                          map (aux false) args)
+    in
+      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
+    end
+  in aux true end
+
+fun formula_for_combformula full_types =
+  let
+    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+      | aux (AConn (c, phis)) = AConn (c, map aux phis)
+      | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
+  in aux end
+
+fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
+  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
+                (type_literals_for_types ctypes_sorts))
+           (formula_for_combformula full_types combformula)
 
 fun problem_line_for_axiom full_types
-        (clause as FOLClause {axiom_name, kind, ...}) =
-  Fof (hol_ident axiom_prefix axiom_name, kind,
-       formula_for_axiom full_types clause)
+        (formula as FOLFormula {formula_name, kind, ...}) =
+  Fof (axiom_prefix ^ ascii_of formula_name, kind,
+       formula_for_axiom full_types formula)
 
 fun problem_line_for_class_rel_clause
         (ClassRelClause {axiom_name, subclass, superclass, ...}) =
@@ -210,23 +242,24 @@
 fun problem_line_for_arity_clause
         (ArityClause {axiom_name, conclLit, premLits, ...}) =
   Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
-       map fo_literal_for_arity_literal (conclLit :: premLits)
-       |> formula_for_fo_literals)
+       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
-        (clause as FOLClause {axiom_name, kind, literals, ...}) =
-  Fof (hol_ident conjecture_prefix axiom_name, kind,
-       map (fo_literal_for_literal full_types) literals
-       |> formula_for_fo_literals |> mk_anot)
+        (FOLFormula {formula_name, kind, combformula, ...}) =
+  Fof (conjecture_prefix ^ formula_name, kind,
+       formula_for_combformula full_types combformula)
 
-fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
-  map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
+fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
+  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_free_type lit =
-  Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit)
+  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
 fun problem_lines_for_free_types conjectures =
   let
-    val litss = map atp_free_type_literals_for_conjecture conjectures
+    val litss = map free_type_literals_for_conjecture conjectures
     val lits = fold (union (op =)) litss []
   in map problem_line_for_free_type lits end
 
@@ -269,7 +302,7 @@
        16383 (* large number *)
      else if full_types then
        0
-     else case strip_prefix const_prefix s of
+     else case strip_prefix_and_undo_ascii const_prefix s of
        SOME s' => num_type_args thy (invert_const s')
      | NONE => 0)
   | min_arity_of _ _ (SOME the_const_tab) s =
@@ -360,11 +393,10 @@
   repair_problem_with_const_table thy explicit_forall full_types
       (const_table_for_problem explicit_apply problem) problem
 
-fun write_tptp_file thy readable_names full_types explicit_apply file
-                    (conjectures, axiom_clauses, extra_clauses, helper_clauses,
-                     class_rel_clauses, arity_clauses) =
+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) =
   let
-    val explicit_forall = true (* FIXME *)
     val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
     val class_rel_lines =
       map problem_line_for_class_rel_clause class_rel_clauses
@@ -373,6 +405,8 @@
     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 =
       [("Relevant facts", axiom_lines),
        ("Class relationships", class_rel_lines),
diff -r ada7d21fde11 -r ae3df22dd70b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jul 27 14:02:15 2010 +0200
@@ -18,6 +18,7 @@
   val maybe_quote : string -> string
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
+  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
 end;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -126,5 +127,11 @@
     | NONE => raise Type.TYPE_MATCH
   end
 
+fun strip_subgoal goal i =
+  let
+    val (t, frees) = Logic.goal_params (prop_of goal) i
+    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
+    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
+  in (rev (map dest_Free frees), hyp_ts, concl_t) end
 
 end;