1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
     1.3 @@ -478,7 +478,6 @@
     1.4                   (the_default default_max_facts max_facts)
     1.5                   Sledgehammer_Fact.no_fact_override hyp_ts concl_t
     1.6            |> #1 (*###*)
     1.7 -          |> map (apfst (apfst (fn name => name ())))
     1.8            |> tap (fn facts =>
     1.9                       "Line " ^ str0 (Position.line_of pos) ^ ": " ^
    1.10                       (if null facts then

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Jan 31 17:54:05 2013 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Jan 31 17:54:05 2013 +0100
     2.3 @@ -136,7 +136,7 @@
     2.4             |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
     2.5                    default_prover (the_default default_max_facts max_facts)
     2.6                    (SOME relevance_fudge) hyp_ts concl_t
     2.7 -            |> map ((fn name => name ()) o fst o fst)
     2.8 +            |> map (fst o fst)
     2.9           val (found_facts, lost_facts) =
    2.10             flat proofs |> sort_distinct string_ord
    2.11             |> map (fn fact => (find_index (curry (op =) fact) facts, fact))

     3.1 --- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 31 17:54:05 2013 +0100
     3.2 +++ b/src/HOL/TPTP/mash_eval.ML	Thu Jan 31 17:54:05 2013 +0100
     3.3 @@ -71,7 +71,7 @@
     3.4      val str_of_method = enclose "  " ": "
     3.5      fun str_of_result method facts ({outcome, run_time, used_facts, ...}
     3.6                                       : prover_result) =
     3.7 -      let val facts = facts |> map (fn ((name, _), _) => name ()) in
     3.8 +      let val facts = facts |> map (fst o fst) in
     3.9          str_of_method method ^
    3.10          (if is_none outcome then
    3.11             "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
    3.12 @@ -111,7 +111,7 @@
    3.13            val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    3.14            val isar_deps = isar_dependencies_of name_tabs th
    3.15            val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    3.16 -          val find_suggs = find_suggested_facts facts
    3.17 +          val find_suggs = find_suggested_facts facts #> map fact_of_raw_fact
    3.18            fun get_facts [] compute = compute facts
    3.19              | get_facts suggs _ = find_suggs suggs
    3.20            val mepo_facts =
    3.21 @@ -121,7 +121,8 @@
    3.22              |> weight_mepo_facts
    3.23            fun mash_of suggs =
    3.24              get_facts suggs (fn _ =>
    3.25 -                find_mash_suggestions slack_max_facts suggs facts [] [] |> fst)
    3.26 +                find_mash_suggestions slack_max_facts suggs facts [] []
    3.27 +                |> fst |> map fact_of_raw_fact)
    3.28              |> weight_mash_facts
    3.29            val mash_isar_facts = mash_of mash_isar_suggs
    3.30            val mash_prover_facts = mash_of mash_prover_suggs
    3.31 @@ -160,6 +161,7 @@
    3.32                    |> map (get #> nickify)
    3.33                    |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    3.34                    |> take (the max_facts)
    3.35 +                  |> map fact_of_raw_fact
    3.36                  val ctxt = ctxt |> set_file_name method prob_dir_name
    3.37                  val res as {outcome, ...} =
    3.38                    run_prover_for_mash ctxt params prover facts goal

     4.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Jan 31 17:54:05 2013 +0100
     4.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Jan 31 17:54:05 2013 +0100
     4.3 @@ -45,8 +45,7 @@
     4.4        |> #1
     4.5      val problem =
     4.6        {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
     4.7 -       facts = facts |> map (apfst (apfst (fn name => name ())))
     4.8 -                     |> map Untranslated_Fact}
     4.9 +       facts = facts |> map Untranslated_Fact}
    4.10    in
    4.11      (case prover params (K (K (K ""))) problem of
    4.12        {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 31 17:54:05 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 31 17:54:05 2013 +0100
     5.3 @@ -10,7 +10,8 @@
     5.4    type status = ATP_Problem_Generate.status
     5.5    type stature = ATP_Problem_Generate.stature
     5.6  
     5.7 -  type fact = ((unit -> string) * stature) * thm
     5.8 +  type raw_fact = ((unit -> string) * stature) * thm
     5.9 +  type fact = (string * stature) * thm
    5.10  
    5.11    type fact_override =
    5.12      {add : (Facts.ref * Attrib.src list) list,
    5.13 @@ -33,12 +34,13 @@
    5.14      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    5.15      -> (((unit -> string) * 'a) * thm) list
    5.16    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    5.17 +  val fact_of_raw_fact : raw_fact -> fact
    5.18    val all_facts :
    5.19      Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    5.20 -    -> status Termtab.table -> fact list
    5.21 +    -> status Termtab.table -> raw_fact list
    5.22    val nearly_all_facts :
    5.23      Proof.context -> bool -> fact_override -> unit Symtab.table
    5.24 -    -> status Termtab.table -> thm list -> term list -> term -> fact list
    5.25 +    -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
    5.26  end;
    5.27  
    5.28  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    5.29 @@ -49,7 +51,8 @@
    5.30  open Metis_Tactic
    5.31  open Sledgehammer_Util
    5.32  
    5.33 -type fact = ((unit -> string) * stature) * thm
    5.34 +type raw_fact = ((unit -> string) * stature) * thm
    5.35 +type fact = (string * stature) * thm
    5.36  
    5.37  type fact_override =
    5.38    {add : (Facts.ref * Attrib.src list) list,
    5.39 @@ -419,6 +422,8 @@
    5.40  fun maybe_filter_no_atps ctxt =
    5.41    not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
    5.42  
    5.43 +fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
    5.44 +
    5.45  fun all_facts ctxt generous ho_atp reserved add_ths chained css =
    5.46    let
    5.47      val thy = Proof_Context.theory_of ctxt

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
     6.3 @@ -7,6 +7,7 @@
     6.4  signature SLEDGEHAMMER_MASH =
     6.5  sig
     6.6    type stature = ATP_Problem_Generate.stature
     6.7 +  type raw_fact = Sledgehammer_Fact.raw_fact
     6.8    type fact = Sledgehammer_Fact.fact
     6.9    type fact_override = Sledgehammer_Fact.fact_override
    6.10    type params = Sledgehammer_Provers.params
    6.11 @@ -62,7 +63,7 @@
    6.12    val isar_dependencies_of :
    6.13      string Symtab.table * string Symtab.table -> thm -> string list
    6.14    val prover_dependencies_of :
    6.15 -    Proof.context -> params -> string -> int -> fact list
    6.16 +    Proof.context -> params -> string -> int -> raw_fact list
    6.17      -> string Symtab.table * string Symtab.table -> thm
    6.18      -> bool * string list
    6.19    val weight_mepo_facts : 'a list -> ('a * real) list
    6.20 @@ -71,8 +72,8 @@
    6.21      int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
    6.22      -> ('b * thm) list * ('b * thm) list
    6.23    val mash_suggested_facts :
    6.24 -    Proof.context -> params -> string -> int -> term list -> term -> fact list
    6.25 -    -> fact list * fact list
    6.26 +    Proof.context -> params -> string -> int -> term list -> term
    6.27 +    -> raw_fact list -> fact list * fact list
    6.28    val mash_learn_proof :
    6.29      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    6.30      -> unit
    6.31 @@ -85,7 +86,7 @@
    6.32    val mash_weight : real
    6.33    val relevant_facts :
    6.34      Proof.context -> params -> string -> int -> fact_override -> term list
    6.35 -    -> term -> fact list -> fact list * fact list * fact list
    6.36 +    -> term -> raw_fact list -> fact list * fact list * fact list
    6.37    val kill_learners : unit -> unit
    6.38    val running_learners : unit -> unit
    6.39  end;
    6.40 @@ -531,8 +532,7 @@
    6.41    let
    6.42      val problem =
    6.43        {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
    6.44 -       facts = facts |> map (apfst (apfst (fn name => name ())))
    6.45 -                     |> map Untranslated_Fact}
    6.46 +       facts = facts |> map Untranslated_Fact}
    6.47    in
    6.48      get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
    6.49                                 problem
    6.50 @@ -687,14 +687,13 @@
    6.51        val goal = goal_of_thm thy th
    6.52        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    6.53        val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    6.54 -      fun nickify ((_, stature), th) =
    6.55 -        ((fn () => nickname_of_thm th, stature), th)
    6.56 +      fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
    6.57        fun is_dep dep (_, th) = nickname_of_thm th = dep
    6.58        fun add_isar_dep facts dep accum =
    6.59          if exists (is_dep dep) accum then
    6.60            accum
    6.61          else case find_first (is_dep dep) facts of
    6.62 -          SOME ((name, status), th) => accum @ [((name, status), th)]
    6.63 +          SOME ((_, status), th) => accum @ [(("", status), th)]
    6.64          | NONE => accum (* shouldn't happen *)
    6.65        val facts =
    6.66          facts
    6.67 @@ -825,7 +824,10 @@
    6.68                                      (parents, feats, hints))
    6.69              end)
    6.70      val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
    6.71 -  in find_mash_suggestions max_facts suggs facts chained unknown end
    6.72 +  in
    6.73 +    find_mash_suggestions max_facts suggs facts chained unknown
    6.74 +    |> pairself (map fact_of_raw_fact)
    6.75 +  end
    6.76  
    6.77  fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
    6.78    let
    6.79 @@ -1099,7 +1101,9 @@
    6.80    if not (subset (op =) (the_list fact_filter, fact_filters)) then
    6.81      error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
    6.82    else if only then
    6.83 -    (facts, facts, facts)
    6.84 +    let val facts = facts |> map fact_of_raw_fact in
    6.85 +      (facts, facts, facts)
    6.86 +    end
    6.87    else if max_facts <= 0 orelse null facts then
    6.88      ([], [], [])
    6.89    else
    6.90 @@ -1129,11 +1133,12 @@
    6.91            else
    6.92              mepoN
    6.93        val add_ths = Attrib.eval_thms ctxt add
    6.94 -      val in_add = member Thm.eq_thm_prop add_ths o snd
    6.95 +      fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
    6.96        fun add_and_take accepts =
    6.97          (case add_ths of
    6.98             [] => accepts
    6.99 -         | _ => (facts |> filter in_add) @ (accepts |> filter_out in_add))
   6.100 +         | _ => (facts |> filter in_add |> map fact_of_raw_fact) @
   6.101 +                (accepts |> filter_out in_add))
   6.102          |> take max_facts
   6.103        fun mepo () =
   6.104          mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Jan 31 17:54:05 2013 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Jan 31 17:54:05 2013 +0100
     7.3 @@ -8,6 +8,7 @@
     7.4  signature SLEDGEHAMMER_MEPO =
     7.5  sig
     7.6    type stature = ATP_Problem_Generate.stature
     7.7 +  type raw_fact = Sledgehammer_Fact.raw_fact
     7.8    type fact = Sledgehammer_Fact.fact
     7.9    type params = Sledgehammer_Provers.params
    7.10    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    7.11 @@ -20,7 +21,7 @@
    7.12      -> string list
    7.13    val mepo_suggested_facts :
    7.14      Proof.context -> params -> string -> int -> relevance_fudge option
    7.15 -    -> term list -> term -> fact list -> fact list
    7.16 +    -> term list -> term -> raw_fact list -> fact list
    7.17  end;
    7.18  
    7.19  structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
    7.20 @@ -337,7 +338,7 @@
    7.21  
    7.22  fun take_most_relevant ctxt max_facts remaining_max
    7.23          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
    7.24 -        (candidates : ((fact * (string * ptype) list) * real) list) =
    7.25 +        (candidates : ((raw_fact * (string * ptype) list) * real) list) =
    7.26    let
    7.27      val max_imperfect =
    7.28        Real.ceil (Math.pow (max_imperfect,
    7.29 @@ -533,6 +534,7 @@
    7.30         relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
    7.31             facts hyp_ts
    7.32             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    7.33 +    |> map fact_of_raw_fact
    7.34    end
    7.35  
    7.36  end;

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
     8.3 @@ -237,7 +237,6 @@
     8.4            |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
     8.5                              hyp_ts concl_t
     8.6            |> #1 (*###*)
     8.7 -          |> map (apfst (apfst (fn name => name ())))
     8.8            |> tap (fn facts =>
     8.9                       if verbose then
    8.10                         label ^ plural_s (length provers) ^ ": " ^