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