# HG changeset patch
# User wenzelm
# Date 1468613514 -7200
# Node ID 79122bdd440447ca2a222172a40b0887b3224fe0
# Parent  cb0882cf150d9122252960c9ced187124b776d5c
clarified markup;

diff -r cb0882cf150d -r 79122bdd4404 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- 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
diff -r cb0882cf150d -r 79122bdd4404 src/HOL/Statespace/StateSpaceEx.thy
--- 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>