src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 57037 c51132be8e16
parent 56303 4cc3f4db3447
child 57053 46000c075d07
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 21 13:52:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 21 14:09:42 2014 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4              SOME name => error ("No such prover: " ^ name ^ ".")
     1.5            | NONE => ())
     1.6          val _ = print "Sledgehammering..."
     1.7 -        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
     1.8 +        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
     1.9  
    1.10          val spying_str_of_factss =
    1.11            commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))