--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Fri Jul 15 15:19:12 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Fri Jul 15 22:11:54 2016 +0200
@@ -60,7 +60,8 @@
fun print_cert cert =
Output.information
("To repeat this proof with a certificate use this command:\n" ^
- Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
+ Active.sendback_markup [Markup.padding_command]
+ ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
fun sos_tac ctxt NONE =
Sum_of_Squares.sos_tac print_cert
--- a/src/HOL/Statespace/StateSpaceEx.thy Fri Jul 15 15:19:12 2016 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy Fri Jul 15 22:11:54 2016 +0200
@@ -234,7 +234,7 @@
ML \<open>
fun make_benchmark n =
- writeln (Active.sendback_markup []
+ writeln (Active.sendback_markup [Markup.padding_command]
("statespace benchmark" ^ string_of_int n ^ " =\n" ^
(cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
\<close>