# HG changeset patch
# User blanchet
# Date 1400674182 -7200
# Node ID c51132be8e1633b4bb34fcc8676dcc33a240fa4e
# Parent  22568fb8916542dae700af678ffad85178008a67
avoid markup-generating @{make_string}

diff -r 22568fb89165 -r c51132be8e16 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 21 13:52:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 21 14:09:42 2014 +0200
@@ -246,7 +246,7 @@
             SOME name => error ("No such prover: " ^ name ^ ".")
           | NONE => ())
         val _ = print "Sledgehammering..."
-        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
+        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
 
         val spying_str_of_factss =
           commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
diff -r 22568fb89165 -r c51132be8e16 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 21 13:52:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 21 14:09:42 2014 +0200
@@ -67,6 +67,7 @@
     -> prover_problem -> prover_result
 
   val SledgehammerN : string
+  val str_of_mode : mode -> string
   val smtN : string
   val overlord_file_location_of_prover : string -> string * string
   val proof_banner : mode -> string -> string
@@ -104,12 +105,19 @@
 open Sledgehammer_Fact
 open Sledgehammer_Proof_Methods
 
-datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
-
 (* Identifier that distinguishes Sledgehammer from other tools that could use
    "Async_Manager". *)
 val SledgehammerN = "Sledgehammer"
 
+datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+
+fun str_of_mode Auto_Try = "Auto Try"
+  | str_of_mode Try = "Try"
+  | str_of_mode Normal = "Normal"
+  | str_of_mode MaSh = "MaSh"
+  | str_of_mode Auto_Minimize = "Auto_Minimize"
+  | str_of_mode Minimize = "Minimize"
+
 val smtN = "smt"
 
 val proof_method_names = [metisN, smtN]