1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -19,10 +19,10 @@
     1.4  open Sledgehammer_Fact
     1.5  open Sledgehammer_Filter_MaSh
     1.6  
     1.7 -val isarN = "Isar"
     1.8 -val iterN = "Iter"
     1.9 -val mashN = "MaSh"
    1.10 -val meshN = "Mesh"
    1.11 +val MePoN = "MePo"
    1.12 +val MaShN = "MaSh"
    1.13 +val MeshN = "Mesh"
    1.14 +val IsarN = "Isar"
    1.15  
    1.16  val max_facts_slack = 2
    1.17  
    1.18 @@ -41,7 +41,7 @@
    1.19      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.20      val facts = all_facts_of thy css_table
    1.21      val all_names = all_names (facts |> map snd)
    1.22 -    val iter_ok = Unsynchronized.ref 0
    1.23 +    val mepo_ok = Unsynchronized.ref 0
    1.24      val mash_ok = Unsynchronized.ref 0
    1.25      val mesh_ok = Unsynchronized.ref 0
    1.26      val isar_ok = Unsynchronized.ref 0
    1.27 @@ -77,13 +77,13 @@
    1.28          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    1.29          val isar_deps = isabelle_dependencies_of all_names th
    1.30          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    1.31 -        val isar_facts = suggested_facts isar_deps facts
    1.32 -        val iter_facts =
    1.33 +        val mepo_facts =
    1.34            Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.35                prover slack_max_facts NONE hyp_ts concl_t facts
    1.36          val mash_facts = facts |> suggested_facts suggs
    1.37 -        val mess = [(iter_facts, []), (mash_facts, [])]
    1.38 +        val mess = [(mepo_facts, []), (mash_facts, [])]
    1.39          val mesh_facts = mesh_facts slack_max_facts mess
    1.40 +        val isar_facts = suggested_facts isar_deps facts
    1.41          fun prove ok heading facts =
    1.42            let
    1.43              val facts =
    1.44 @@ -94,17 +94,17 @@
    1.45                run_prover_for_mash ctxt params prover facts goal
    1.46              val _ = if is_none outcome then ok := !ok + 1 else ()
    1.47            in str_of_res heading facts res end
    1.48 -        val iter_s = prove iter_ok iterN iter_facts
    1.49 -        val mash_s = prove mash_ok mashN mash_facts
    1.50 -        val mesh_s = prove mesh_ok meshN mesh_facts
    1.51 -        val isar_s = prove isar_ok isarN isar_facts
    1.52 +        val mepo_s = prove mepo_ok MePoN mepo_facts
    1.53 +        val mash_s = prove mash_ok MaShN mash_facts
    1.54 +        val mesh_s = prove mesh_ok MeshN mesh_facts
    1.55 +        val isar_s = prove isar_ok IsarN isar_facts
    1.56        in
    1.57 -        ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, mesh_s,
    1.58 +        ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
    1.59           isar_s]
    1.60          |> cat_lines |> tracing
    1.61        end
    1.62      fun total_of heading ok n =
    1.63 -      " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
    1.64 +      "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
    1.65        Real.fmt (StringCvt.FIX (SOME 1))
    1.66                 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
    1.67      val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
    1.68 @@ -119,10 +119,10 @@
    1.69      tracing ("Options: " ^ commas options);
    1.70      List.app solve_goal (tag_list 1 lines);
    1.71      ["Successes (of " ^ string_of_int n ^ " goals)",
    1.72 -     total_of iterN iter_ok n,
    1.73 -     total_of mashN mash_ok n,
    1.74 -     total_of meshN mesh_ok n,
    1.75 -     total_of isarN isar_ok n]
    1.76 +     total_of MePoN mepo_ok n,
    1.77 +     total_of MaShN mash_ok n,
    1.78 +     total_of MeshN mesh_ok n,
    1.79 +     total_of IsarN isar_ok n]
    1.80      |> cat_lines |> tracing
    1.81    end
    1.82