src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 52697 6fb98a20c349
parent 52196 2281f33e8da6
child 53082 369e39511555
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 18 13:12:54 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 18 20:53:22 2013 +0200
     1.3 @@ -955,7 +955,8 @@
     1.4        |> drop (length old_facts)
     1.5      end
     1.6  
     1.7 -fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
     1.8 +fun sendback sub =
     1.9 +  Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
    1.10  
    1.11  val commit_timeout = seconds 30.0
    1.12