src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
   val infinite_timeout : Time.time
   val time_mult : real -> Time.time -> Time.time
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
-  val spying : bool -> (unit -> string * string) -> unit
   val subgoal_count : Proof.state -> int
   val reserved_isar_keyword_table : unit -> unit Symtab.table
   val thms_in_proof :
     (string Symtab.table * string Symtab.table) option -> thm -> string list
   val thms_of_name : Proof.context -> string -> thm list
   val one_day : Time.time
   val one_year : Time.time
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
+  val hackish_string_of_term : Proof.context -> term -> string
+  val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
 
   (** extrema **)
   val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
   val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
   val max_list : ('a * 'a -> order) -> 'a list -> 'a option

       if is_none secs orelse Real.< (the secs, 0.0) then
         error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
                \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
       else
         SOME (seconds (the secs))
-    end
-
-val spying_version = "a"
-
-fun spying false _ = ()
-  | spying true f =
-    let val (tool, message) = f () in
-      File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
-        (spying_version ^ " " ^ timestamp () ^ ": " ^ tool ^ ": " ^ message ^ "\n")
     end
 
 val subgoal_count = Try.subgoal_count
 
 fun reserved_isar_keyword_table () =

 
 fun with_vanilla_print_mode f x =
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                            (print_mode_value ())) f x
 
+fun hackish_string_of_term ctxt =
+  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
+
+val spying_version = "b"
+
+fun spying false _ = ()
+  | spying true f =
+    let
+      val (state, i, tool, message) = f ()
+      val ctxt = Proof.context_of state
+      val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i
+      val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
+    in
+      File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
+        (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
+    end
+
 (** extrema **)
 
 fun max ord x y = case ord(x,y) of LESS => y | _ => x
 
 fun max_option ord = max (option_ord ord)