src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

 signature SLEDGEHAMMER_RUN =
 sig
   type relevance_override = Sledgehammer_Filter.relevance_override
   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
   type params = Sledgehammer_Provers.params
-
-  (* for experimentation purposes -- do not use in production code *)
-  val show_facts_in_proofs : bool Unsynchronized.ref
 
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
 end;

   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
   (if blocking then
      ""
    else
      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
-
-val show_facts_in_proofs = Unsynchronized.ref false
 
 val implicit_minimization_threshold = 50
 
 fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
                auto minimize_command only

                               (map (apsnd single o untranslated_fact) facts))
                      |>> Option.map (map fst)
                    else
                      (SOME used_facts, message)
                  val _ =
-                   case (debug orelse !show_facts_in_proofs, used_facts) of
+                   case (debug, used_facts) of
                      (true, SOME (used_facts as _ :: _)) =>
                      facts ~~ (0 upto length facts - 1)
                      |> map (fn (fact, j) =>
                                 fact |> untranslated_fact |> apsnd (K j))
                      |> filter_used_facts used_facts