tuned code
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 5525185f5d7da4ab6
parent 55250 982e082cd2ba
child 55252 0dc4993b4f56
tuned code
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -39,22 +39,11 @@
     1.4    let
     1.5      val ctxt = ctxt |> Config.put show_markup true
     1.6      val assms = op @ assmsp
     1.7 -    val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
     1.8 -    val nr_of_assms = length assms
     1.9 -    val assms = assms
    1.10 -      |> map (Display.pretty_thm ctxt)
    1.11 -      |> (fn [] => Pretty.str ""
    1.12 -           | [a] => a
    1.13 -           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
    1.14 -    val concl = concl |> Syntax.pretty_term ctxt
    1.15 -    val trace_list = []
    1.16 -      |> cons concl
    1.17 -      |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
    1.18 -      |> cons assms
    1.19 -      |> cons time
    1.20 -    val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
    1.21 +    val time = Pretty.str ("[" ^ string_of_play_outcome result ^ "]")
    1.22 +    val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
    1.23 +    val concl = Syntax.pretty_term ctxt concl
    1.24    in
    1.25 -    tracing (Pretty.string_of pretty_trace)
    1.26 +    tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
    1.27    end
    1.28  
    1.29  fun take_time timeout tac arg =