1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 16:04:15 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 22 10:25:07 2010 +0100
     1.3 @@ -174,14 +174,14 @@
     1.4  val vampire_max_new_clauses = 60;
     1.5  val vampire_insert_theory_const = false;
     1.6  
     1.7 -fun vampire_prover_config full : prover_config =
     1.8 +fun vampire_prover_config isar : prover_config =
     1.9   {command = Path.explode "$VAMPIRE_HOME/vampire",
    1.10    arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
    1.11      " -t " ^ string_of_int timeout),
    1.12    failure_strs = vampire_failure_strs,
    1.13    max_new_clauses = vampire_max_new_clauses,
    1.14    insert_theory_const = vampire_insert_theory_const,
    1.15 -  emit_structured_proof = full};
    1.16 +  emit_structured_proof = isar};
    1.17  
    1.18  val vampire = tptp_prover ("vampire", vampire_prover_config false);
    1.19  val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
    1.20 @@ -196,14 +196,14 @@
    1.21  val eprover_max_new_clauses = 100;
    1.22  val eprover_insert_theory_const = false;
    1.23  
    1.24 -fun eprover_config full : prover_config =
    1.25 +fun eprover_config isar : prover_config =
    1.26   {command = Path.explode "$E_HOME/eproof",
    1.27    arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
    1.28      " --silent --cpu-limit=" ^ string_of_int timeout),
    1.29    failure_strs = eprover_failure_strs,
    1.30    max_new_clauses = eprover_max_new_clauses,
    1.31    insert_theory_const = eprover_insert_theory_const,
    1.32 -  emit_structured_proof = full};
    1.33 +  emit_structured_proof = isar};
    1.34  
    1.35  val eprover = tptp_prover ("e", eprover_config false);
    1.36  val eprover_isar = tptp_prover ("e_isar", eprover_config true);

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Mar 19 16:04:15 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Mar 22 10:25:07 2010 +0100
     2.3 @@ -463,7 +463,8 @@
     2.4  fun neg_skolemize_tac ctxt =
     2.5    EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
     2.6  
     2.7 -val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
     2.8 +val neg_clausify =
     2.9 +  Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
    2.10  
    2.11  fun neg_conjecture_clauses ctxt st0 n =
    2.12    let

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Mar 19 16:04:15 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 22 10:25:07 2010 +0100
     3.3 @@ -333,26 +333,30 @@
     3.4              then SOME ctm else perm ctms
     3.5    in perm end;
     3.6  
     3.7 -fun have_or_show "show " _ = "show \""
     3.8 -  | have_or_show have lname = have ^ lname ^ ": \""
     3.9 -
    3.10  (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
    3.11    ATP may have their literals reordered.*)
    3.12 -fun isar_lines ctxt ctms =
    3.13 -  let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
    3.14 -      val _ = trace_proof_msg (K "\n\nisar_lines: start\n")
    3.15 -      fun doline _ (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
    3.16 -           (case permuted_clause t ctms of
    3.17 -                SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
    3.18 -              | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
    3.19 -        | doline have (lname, t, deps) =
    3.20 -            have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
    3.21 -            "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
    3.22 -      fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
    3.23 -        | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
    3.24 -  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
    3.25 +fun isar_proof_body ctxt ctms =
    3.26 +  let
    3.27 +    val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
    3.28 +    val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
    3.29 +    fun have_or_show "show" _ = "show \""
    3.30 +      | have_or_show have lname = have ^ " " ^ lname ^ ": \""
    3.31 +    fun do_line _ (lname, t, []) =
    3.32 +       (* No deps: it's a conjecture clause, with no proof. *)
    3.33 +       (case permuted_clause t ctms of
    3.34 +          SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
    3.35 +        | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
    3.36 +                              [t]))
    3.37 +      | do_line have (lname, t, deps) =
    3.38 +        have_or_show have lname ^
    3.39 +        string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
    3.40 +        "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
    3.41 +    fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
    3.42 +      | do_lines ((lname, t, deps) :: lines) =
    3.43 +        do_line "have" (lname, t, deps) :: do_lines lines
    3.44 +  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
    3.45  
    3.46 -fun notequal t (_,t',_) = not (t aconv t');
    3.47 +fun unequal t (_, t', _) = not (t aconv t');
    3.48  
    3.49  (*No "real" literals means only type information*)
    3.50  fun eq_types t = t aconv HOLogic.true_const;
    3.51 @@ -368,7 +372,7 @@
    3.52        if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
    3.53        then map (replace_deps (lno, [])) lines
    3.54        else
    3.55 -       (case take_prefix (notequal t) lines of
    3.56 +       (case take_prefix (unequal t) lines of
    3.57             (_,[]) => lines                  (*no repetition of proof line*)
    3.58           | (pre, (lno', _, _) :: post) =>   (*repetition: replace later line by earlier one*)
    3.59               pre @ map (replace_deps (lno', [lno])) post)
    3.60 @@ -378,7 +382,7 @@
    3.61        if eq_types t then (lno, t, deps) :: lines
    3.62        (*Type information will be deleted later; skip repetition test.*)
    3.63        else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
    3.64 -      case take_prefix (notequal t) lines of
    3.65 +      case take_prefix (unequal t) lines of
    3.66           (_,[]) => (lno, t, deps) :: lines  (*no repetition of proof line*)
    3.67         | (pre, (lno', t', _) :: post) =>
    3.68             (lno, t', deps) ::               (*repetition: replace later line by earlier one*)
    3.69 @@ -450,10 +454,10 @@
    3.70      val ccls = map forall_intr_vars ccls
    3.71      val _ = app (fn th => trace_proof_msg
    3.72                                (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
    3.73 -    val isar_lines = isar_lines ctxt (map prop_of ccls)
    3.74 -                                (stringify_deps thm_names [] lines)
    3.75 +    val body = isar_proof_body ctxt (map prop_of ccls)
    3.76 +                               (stringify_deps thm_names [] lines)
    3.77      val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
    3.78 -  in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end
    3.79 +  in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
    3.80    handle STREE _ => error "Could not extract proof (ATP output malformed?)";
    3.81  
    3.82  

     4.1 --- a/src/HOL/Tools/meson.ML	Fri Mar 19 16:04:15 2010 +0100
     4.2 +++ b/src/HOL/Tools/meson.ML	Mon Mar 22 10:25:07 2010 +0100
     4.3 @@ -18,6 +18,7 @@
     4.4    val make_nnf: Proof.context -> thm -> thm
     4.5    val skolemize: Proof.context -> thm -> thm
     4.6    val is_fol_term: theory -> term -> bool
     4.7 +  val make_clauses_unsorted: thm list -> thm list
     4.8    val make_clauses: thm list -> thm list
     4.9    val make_horns: thm list -> thm list
    4.10    val best_prolog_tac: (thm -> int) -> thm list -> tactic
    4.11 @@ -560,7 +561,8 @@
    4.12  
    4.13  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    4.14    The resulting clauses are HOL disjunctions.*)
    4.15 -fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
    4.16 +fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
    4.17 +val make_clauses = sort_clauses o make_clauses_unsorted;
    4.18  
    4.19  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    4.20  fun make_horns ths =