src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 
 (* FIXME: use "Generic_Data" *)
 structure Data = Theory_Data
 (
   type T = raw_param list
-  val empty =
-    default_default_params
-    |> getenv "SLEDGEHAMMER_SPY" = "yes" ? AList.update (op =) ("spy", "true")
-    |> map (apsnd single)
+  val empty = default_default_params |> map (apsnd single)
   val extend = I
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low

         SOME "smart" => NONE
       | _ => SOME (lookup' name)
     val debug = mode <> Auto_Try andalso lookup_bool "debug"
     val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
-    val spy = lookup_bool "spy"
+    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
     val blocking =
       Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
       lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> mode = Auto_Try ? single o hd