1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4    end
     1.5  
     1.6  fun all_non_tautological_facts_of thy css_table =
     1.7 -  Sledgehammer_Fact.all_facts_of thy css_table
     1.8 +  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     1.9    |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
    1.10  
    1.11  fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =

     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -39,7 +39,7 @@
     2.4      val path = file_name |> Path.explode
     2.5      val lines = path |> File.read_lines
     2.6      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     2.7 -    val facts = all_facts_of thy css_table
     2.8 +    val facts = all_facts_of (Proof_Context.init_global thy) css_table
     2.9      val all_names = all_names (facts |> map snd)
    2.10      val mepo_ok = Unsynchronized.ref 0
    2.11      val mash_ok = Unsynchronized.ref 0

     3.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     3.3 @@ -63,7 +63,7 @@
     3.4          val _ = File.append path s
     3.5        in [fact] end
     3.6      val thy_map =
     3.7 -      all_facts_of thy Termtab.empty
     3.8 +      all_facts_of (Proof_Context.init_global thy) Termtab.empty
     3.9        |> not include_thy ? filter_out (has_thy thy o snd)
    3.10        |> thy_map_from_facts
    3.11      fun do_thy facts =
    3.12 @@ -79,7 +79,7 @@
    3.13      val _ = File.write path ""
    3.14      val css_table = clasimpset_rule_table_of ctxt
    3.15      val facts =
    3.16 -      all_facts_of thy css_table
    3.17 +      all_facts_of (Proof_Context.init_global thy) css_table
    3.18        |> not include_thy ? filter_out (has_thy thy o snd)
    3.19      fun do_fact ((_, stature), th) =
    3.20        let
    3.21 @@ -95,7 +95,7 @@
    3.22      val path = file_name |> Path.explode
    3.23      val _ = File.write path ""
    3.24      val ths =
    3.25 -      all_facts_of thy Termtab.empty
    3.26 +      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    3.27        |> not include_thy ? filter_out (has_thy thy o snd)
    3.28        |> map snd
    3.29      val all_names = all_names ths
    3.30 @@ -114,7 +114,7 @@
    3.31      val _ = File.write path ""
    3.32      val prover = hd provers
    3.33      val facts =
    3.34 -      all_facts_of thy Termtab.empty
    3.35 +      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    3.36        |> not include_thy ? filter_out (has_thy thy o snd)
    3.37      val ths = facts |> map snd
    3.38      val all_names = all_names ths
    3.39 @@ -132,7 +132,7 @@
    3.40      val path = file_name |> Path.explode
    3.41      val _ = File.write path ""
    3.42      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.43 -    val facts = all_facts_of thy css_table
    3.44 +    val facts = all_facts_of (Proof_Context.init_global thy) css_table
    3.45      val (new_facts, old_facts) =
    3.46        facts |> List.partition (has_thy thy o snd)
    3.47              |>> sort (thm_ord o pairself snd)
    3.48 @@ -162,7 +162,7 @@
    3.49      val _ = File.write path ""
    3.50      val prover = hd provers
    3.51      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.52 -    val facts = all_facts_of thy css_table
    3.53 +    val facts = all_facts_of (Proof_Context.init_global thy) css_table
    3.54      val (new_facts, old_facts) =
    3.55        facts |> List.partition (has_thy thy o snd)
    3.56              |>> sort (thm_ord o pairself snd)

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jul 20 22:19:46 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jul 20 22:19:46 2012 +0200
     4.3 @@ -23,12 +23,13 @@
     4.4    val fact_from_ref :
     4.5      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     4.6      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     4.7 +  val backquote_thm : thm -> string
     4.8    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
     4.9    val maybe_instantiate_inducts :
    4.10      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    4.11      -> (((unit -> string) * 'a) * thm) list
    4.12    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    4.13 -  val all_facts_of : theory -> status Termtab.table -> fact list
    4.14 +  val all_facts_of : Proof.context -> status Termtab.table -> fact list
    4.15    val nearly_all_facts :
    4.16      Proof.context -> bool -> fact_override -> unit Symtab.table
    4.17      -> status Termtab.table -> thm list -> term list -> term -> fact list
    4.18 @@ -212,9 +213,9 @@
    4.19      is_that_fact thm
    4.20    end
    4.21  
    4.22 -fun hackish_string_for_term ctxt t =
    4.23 +fun hackish_string_for_term thy t =
    4.24    Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    4.25 -                   (print_mode_value ())) (Syntax.string_of_term ctxt) t
    4.26 +                   (print_mode_value ())) (Syntax.string_of_term_global thy) t
    4.27    |> String.translate (fn c => if Char.isPrint c then str c else "")
    4.28    |> simplify_spaces
    4.29  
    4.30 @@ -240,6 +241,11 @@
    4.31            (Term.add_vars t [] |> sort_wrt (fst o fst))
    4.32    |> fst
    4.33  
    4.34 +fun backquote_thm th =
    4.35 +  th |> prop_of |> close_form
    4.36 +     |> hackish_string_for_term (theory_of_thm th)
    4.37 +     |> backquote
    4.38 +
    4.39  fun clasimpset_rule_table_of ctxt =
    4.40    let
    4.41      val thy = Proof_Context.theory_of ctxt
    4.42 @@ -302,13 +308,14 @@
    4.43  
    4.44  fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
    4.45    let
    4.46 +    val thy = Proof_Context.theory_of ctxt
    4.47      fun varify_noninducts (t as Free (s, T)) =
    4.48          if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
    4.49        | varify_noninducts t = t
    4.50      val p_inst =
    4.51        concl_prop |> map_aterms varify_noninducts |> close_form
    4.52                   |> lambda (Free ind_x)
    4.53 -                 |> hackish_string_for_term ctxt
    4.54 +                 |> hackish_string_for_term thy
    4.55    in
    4.56      ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
    4.57        stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
    4.58 @@ -374,8 +381,6 @@
    4.59          else
    4.60            let
    4.61              val multi = length ths > 1
    4.62 -            val backquote_thm =
    4.63 -              backquote o hackish_string_for_term ctxt o close_form o prop_of
    4.64              fun check_thms a =
    4.65                case try (Proof_Context.get_thms ctxt) a of
    4.66                  NONE => false
    4.67 @@ -392,7 +397,7 @@
    4.68                               val new =
    4.69                                 (((fn () =>
    4.70                                       if name0 = "" then
    4.71 -                                       th |> backquote_thm
    4.72 +                                       backquote_thm th
    4.73                                       else
    4.74                                         [Facts.extern ctxt facts name0,
    4.75                                          Name_Space.extern ctxt full_space name0]
    4.76 @@ -415,11 +420,9 @@
    4.77               |> op @
    4.78    end
    4.79  
    4.80 -fun all_facts_of thy css_table =
    4.81 -  let val ctxt = Proof_Context.init_global thy in
    4.82 -    all_facts ctxt false Symtab.empty [] [] css_table
    4.83 -    |> rev (* try to restore the original order of facts, for MaSh *)
    4.84 -  end
    4.85 +fun all_facts_of ctxt css_table =
    4.86 +  all_facts ctxt false Symtab.empty [] [] css_table
    4.87 +  |> rev (* try to restore the original order of facts, for MaSh *)
    4.88  
    4.89  fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
    4.90                       hyp_ts concl_t =

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     5.3 @@ -101,9 +101,10 @@
     5.4  val relearn_atpN = "relearn_atp"
     5.5  
     5.6  fun mash_home () = getenv "MASH_HOME"
     5.7 -fun mash_state_dir () =
     5.8 +fun mash_model_dir () =
     5.9    getenv "ISABELLE_HOME_USER" ^ "/mash"
    5.10    |> tap (Isabelle_System.mkdir o Path.explode)
    5.11 +val mash_state_dir = mash_model_dir
    5.12  fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
    5.13  
    5.14  
    5.15 @@ -115,14 +116,14 @@
    5.16      String.str c
    5.17    else
    5.18      (* fixed width, in case more digits follow *)
    5.19 -    "\\" ^ stringN_of_int 3 (Char.ord c)
    5.20 +    "$" ^ stringN_of_int 3 (Char.ord c)
    5.21  
    5.22  fun unmeta_chars accum [] = String.implode (rev accum)
    5.23 -  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
    5.24 +  | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) =
    5.25      (case Int.fromString (String.implode [d1, d2, d3]) of
    5.26         SOME n => unmeta_chars (Char.chr n :: accum) cs
    5.27       | NONE => "" (* error *))
    5.28 -  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
    5.29 +  | unmeta_chars _ (#"$" :: _) = "" (* error *)
    5.30    | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
    5.31  
    5.32  val escape_meta = String.translate meta_char
    5.33 @@ -149,13 +150,16 @@
    5.34  val local_prefix = "local" ^ Long_Name.separator
    5.35  
    5.36  fun nickname_of th =
    5.37 -  let val hint = Thm.get_name_hint th in
    5.38 -    (* FIXME: There must be a better way to detect local facts. *)
    5.39 -    case try (unprefix local_prefix) hint of
    5.40 -      SOME suff =>
    5.41 -      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
    5.42 -    | NONE => hint
    5.43 -  end
    5.44 +  if Thm.has_name_hint th then
    5.45 +    let val hint = Thm.get_name_hint th in
    5.46 +      (* FIXME: There must be a better way to detect local facts. *)
    5.47 +      case try (unprefix local_prefix) hint of
    5.48 +        SOME suf =>
    5.49 +        parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
    5.50 +      | NONE => hint
    5.51 +    end
    5.52 +  else
    5.53 +    backquote_thm th
    5.54  
    5.55  fun suggested_facts suggs facts =
    5.56    let
    5.57 @@ -369,56 +373,47 @@
    5.58  
    5.59  (*** Low-level communication with MaSh ***)
    5.60  
    5.61 +(* more friendly than "try o File.rm" for those who keep the files open in their
    5.62 +   text editor *)
    5.63 +fun wipe_out file = File.write file ""
    5.64 +
    5.65  fun write_file (xs, f) file =
    5.66    let val path = Path.explode file in
    5.67 -    File.write path "";
    5.68 +    wipe_out path;
    5.69      xs |> chunk_list 500
    5.70         |> List.app (File.append path o space_implode "" o map f)
    5.71    end
    5.72  
    5.73 -fun mash_info overlord =
    5.74 -  if overlord then (getenv "ISABELLE_HOME_USER", "")
    5.75 -  else (getenv "ISABELLE_TMP", serial_string ())
    5.76 -
    5.77 -fun and_rm_files overlord flags files =
    5.78 -  if overlord then
    5.79 -    ""
    5.80 -  else
    5.81 -    " && rm -f" ^ flags ^ " -- " ^
    5.82 -    space_implode " " (map File.shell_quote files)
    5.83 -
    5.84 -fun run_mash ctxt overlord (temp_dir, serial) async core =
    5.85 +fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
    5.86    let
    5.87 -    val log_file = temp_dir ^ "/mash_log" ^ serial
    5.88 +    val (temp_dir, serial) =
    5.89 +      if overlord then (getenv "ISABELLE_HOME_USER", "")
    5.90 +      else (getenv "ISABELLE_TMP", serial_string ())
    5.91 +    val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
    5.92      val err_file = temp_dir ^ "/mash_err" ^ serial
    5.93 -    val command =
    5.94 -      "(" ^ mash_home () ^ "/mash --quiet --outputDir " ^ mash_state_dir () ^
    5.95 -      " --log " ^ log_file ^ " " ^ core ^ ") 2>&1 > " ^ err_file ^
    5.96 -      and_rm_files overlord "" [log_file, err_file] ^
    5.97 -      (if async then " &" else "")
    5.98 -  in
    5.99 -    trace_msg ctxt (fn () =>
   5.100 -        (if async then "Launching " else "Running ") ^ command);
   5.101 -    write_file ([], K "") log_file;
   5.102 -    write_file ([], K "") err_file;
   5.103 -    Isabelle_System.bash command;
   5.104 -    if not async then trace_msg ctxt (K "Done") else ()
   5.105 -  end
   5.106 -
   5.107 -fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
   5.108 -  let
   5.109 -    val info as (temp_dir, serial) = mash_info overlord
   5.110      val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
   5.111      val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   5.112 +    val core =
   5.113 +      "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   5.114 +      " --numberOfPredictions " ^ string_of_int max_suggs ^
   5.115 +      (if save then " --saveModel" else "")
   5.116 +    val command =
   5.117 +      mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
   5.118 +      " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
   5.119    in
   5.120      write_file ([], K "") sugg_file;
   5.121      write_file write_cmds cmd_file;
   5.122 -    run_mash ctxt overlord info false
   5.123 -             ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   5.124 -              " --numberOfPredictions " ^ string_of_int max_suggs ^
   5.125 -              (if save then " --saveModel" else "") ^
   5.126 -              (and_rm_files overlord "" [sugg_file, cmd_file]));
   5.127 -    read_suggs (fn () => File.read_lines (Path.explode sugg_file))
   5.128 +    trace_msg ctxt (fn () => "Running " ^ command);
   5.129 +    Isabelle_System.bash command;
   5.130 +    read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
   5.131 +    |> tap (fn _ => trace_msg ctxt (fn () =>
   5.132 +           case try File.read (Path.explode err_file) of
   5.133 +             NONE => "Done"
   5.134 +           | SOME "" => "Done"
   5.135 +           | SOME s => "Error: " ^ elide_string 1000 s))
   5.136 +    |> not overlord
   5.137 +       ? tap (fn _ => List.app (wipe_out o Path.explode)
   5.138 +                               [err_file, sugg_file, cmd_file])
   5.139    end
   5.140  
   5.141  fun str_of_update (name, parents, feats, deps) =
   5.142 @@ -429,24 +424,28 @@
   5.143    "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
   5.144  
   5.145  fun mash_CLEAR ctxt =
   5.146 -  let val path = mash_state_dir () |> Path.explode in
   5.147 +  let val path = mash_model_dir () |> Path.explode in
   5.148      trace_msg ctxt (K "MaSh CLEAR");
   5.149 -    File.fold_dir (fn file => fn () =>
   5.150 -                      File.rm (Path.append path (Path.basic file)))
   5.151 -                  path ()
   5.152 +    File.fold_dir (fn file => fn _ =>
   5.153 +                      try File.rm (Path.append path (Path.basic file)))
   5.154 +                  path NONE;
   5.155 +    ()
   5.156    end
   5.157  
   5.158  fun mash_ADD _ _ [] = ()
   5.159    | mash_ADD ctxt overlord upds =
   5.160      (trace_msg ctxt (fn () => "MaSh ADD " ^
   5.161           elide_string 1000 (space_implode " " (map #1 upds)));
   5.162 -     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
   5.163 +     run_mash_tool ctxt overlord true 0 (upds, str_of_update) (K ()))
   5.164  
   5.165  fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
   5.166    (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
   5.167 -   run_mash_commands ctxt overlord false  max_suggs
   5.168 +   run_mash_tool ctxt overlord false max_suggs
   5.169         ([query], str_of_query)
   5.170 -       (fn suggs => snd (extract_query (List.last (suggs ()))))
   5.171 +       (fn suggs =>
   5.172 +           case suggs () of
   5.173 +             [] => []
   5.174 +           | suggs => snd (extract_query (List.last suggs)))
   5.175     handle List.Empty => [])
   5.176  
   5.177  
   5.178 @@ -529,8 +528,7 @@
   5.179  
   5.180  fun mash_unlearn ctxt =
   5.181    Synchronized.change global_state (fn _ =>
   5.182 -      (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
   5.183 -       (true, empty_state)))
   5.184 +      (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
   5.185  
   5.186  end
   5.187  
   5.188 @@ -642,16 +640,20 @@
   5.189              |> sort (thm_ord o pairself snd)
   5.190      val num_new_facts = length new_facts
   5.191    in
   5.192 -    "MaShing" ^
   5.193      (if not auto then
   5.194 -       " " ^ string_of_int num_new_facts ^ " fact" ^
   5.195 -       plural_s num_new_facts ^
   5.196 -       (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "")
   5.197 +       "MaShing" ^
   5.198 +       (if not auto then
   5.199 +          " " ^ string_of_int num_new_facts ^ " fact" ^
   5.200 +          plural_s num_new_facts ^
   5.201 +          (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")"
   5.202 +           else "")
   5.203 +        else
   5.204 +          "") ^ "..."
   5.205       else
   5.206 -       "") ^ "..."
   5.207 +       "")
   5.208      |> Output.urgent_message;
   5.209      if null new_facts then
   5.210 -      if verbose orelse not auto then
   5.211 +      if not auto then
   5.212          "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
   5.213          sendback relearn_atpN ^ "  to learn from scratch."
   5.214        else
   5.215 @@ -694,6 +696,7 @@
   5.216                  (if atp then atp_dependencies_of ctxt params prover auto facts
   5.217                   else isar_dependencies_of) all_names th
   5.218                  |> trim_deps
   5.219 +              val n = n |> not (null deps) ? Integer.add 1
   5.220                val upds = (name, parents, feats, deps) :: upds
   5.221                val (upds, next_commit) =
   5.222                  if Time.> (Timer.checkRealTimer timer, next_commit) then
   5.223 @@ -702,7 +705,7 @@
   5.224                    (upds, next_commit)
   5.225                val timed_out =
   5.226                  Time.> (Timer.checkRealTimer timer, learn_timeout)
   5.227 -            in (upds, ([name], n + 1, next_commit, timed_out)) end
   5.228 +            in (upds, ([name], n, next_commit, timed_out)) end
   5.229          val parents = parents_wrt_facts facts fact_graph
   5.230          val (upds, (_, n, _, _)) =
   5.231            ([], (parents, 0, next_commit_time (), false))
   5.232 @@ -710,7 +713,7 @@
   5.233        in
   5.234          commit true upds;
   5.235          if verbose orelse not auto then
   5.236 -          "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
   5.237 +          "Learned " ^ string_of_int n ^ " nontrivial proof" ^ plural_s n ^
   5.238            (if verbose then
   5.239               " in " ^ string_from_time (Timer.checkRealTimer timer)
   5.240             else
   5.241 @@ -722,9 +725,8 @@
   5.242  
   5.243  fun mash_learn ctxt (params as {provers, ...}) atp =
   5.244    let
   5.245 -    val thy = Proof_Context.theory_of ctxt
   5.246      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   5.247 -    val facts = all_facts_of thy css_table
   5.248 +    val facts = all_facts_of ctxt css_table
   5.249    in
   5.250       mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
   5.251       |> Output.urgent_message

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     6.3 @@ -256,7 +256,7 @@
     6.4    end
     6.5  
     6.6  fun maybe_minimize ctxt mode do_learn name
     6.7 -        (params as {debug, verbose, isar_proof, minimize, ...})
     6.8 +        (params as {verbose, isar_proof, minimize, ...})
     6.9          ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    6.10          (result as {outcome, used_facts, run_time, preplay, message,
    6.11                      message_tail} : prover_result) =
    6.12 @@ -310,19 +310,8 @@
    6.13      in
    6.14        case used_facts of
    6.15          SOME used_facts =>
    6.16 -        (if debug andalso not (null used_facts) then
    6.17 -           tag_list 1 facts
    6.18 -           |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
    6.19 -           |> filter_used_facts used_facts
    6.20 -           |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
    6.21 -           |> commas
    6.22 -           |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
    6.23 -                       " proof (of " ^ string_of_int (length facts) ^ "): ") "."
    6.24 -           |> Output.urgent_message
    6.25 -         else
    6.26 -           ();
    6.27 -         {outcome = NONE, used_facts = used_facts, run_time = run_time,
    6.28 -          preplay = preplay, message = message, message_tail = message_tail})
    6.29 +        {outcome = NONE, used_facts = used_facts, run_time = run_time,
    6.30 +         preplay = preplay, message = message, message_tail = message_tail}
    6.31        | NONE => result
    6.32      end
    6.33  

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     7.3 @@ -84,12 +84,24 @@
     7.4                    ? filter_out (curry (op =) Induction o snd o snd o fst
     7.5                                  o untranslated_fact)
     7.6                 |> take num_facts}
     7.7 +    fun print_used_facts used_facts =
     7.8 +      tag_list 1 facts
     7.9 +      |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
    7.10 +      |> filter_used_facts used_facts
    7.11 +      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
    7.12 +      |> commas
    7.13 +      |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
    7.14 +                  " proof (of " ^ string_of_int (length facts) ^ "): ") "."
    7.15 +      |> Output.urgent_message
    7.16      fun really_go () =
    7.17        problem
    7.18        |> get_minimizing_prover ctxt mode
    7.19               (mash_learn_proof ctxt params name (prop_of goal)
    7.20                                 (map untranslated_fact facts))
    7.21               name params minimize_command
    7.22 +      |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
    7.23 +                           print_used_facts used_facts
    7.24 +                         | _ => ())
    7.25        |> (fn {outcome, preplay, message, message_tail, ...} =>
    7.26               (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    7.27                else if is_some outcome then noneN
    7.28 @@ -228,7 +240,7 @@
    7.29                              hyp_ts concl_t
    7.30            |> map (apfst (apfst (fn name => name ())))
    7.31            |> tap (fn facts =>
    7.32 -                     if debug then
    7.33 +                     if verbose then
    7.34                         label ^ plural_s (length provers) ^ ": " ^
    7.35                         (if null facts then
    7.36                            "Found no relevant facts."