src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 17 16:55:27 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 17 18:23:56 2010 +0100
@@ -577,6 +577,7 @@
 
 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