# HG changeset patch
# User blanchet
# Date 1292623793 -3600
# Node ID ff38ea43aadaf7619466eabe3bb62c51ccaf5106
# Parent  13972ced98d99964ad1968dee57d6445598ea7b1
remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)

diff -r 13972ced98d9 -r ff38ea43aada src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 17 22:15:08 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 17 23:09:53 2010 +0100
@@ -577,7 +577,6 @@
 
 fun invoke args =
   let
-    val _ = Sledgehammer_Run.show_facts_in_proofs := true
     val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
   in Mirabelle.register (init, sledgehammer_action args, done) end
 
diff -r 13972ced98d9 -r ff38ea43aada src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Dec 17 22:15:08 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Dec 17 23:09:53 2010 +0100
@@ -12,9 +12,6 @@
   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
@@ -42,8 +39,6 @@
    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, ...})
@@ -79,7 +74,7 @@
                    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) =>