src/HOL/Statespace/StateSpaceEx.thy

--- a/src/HOL/Statespace/StateSpaceEx.thy	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Sat Jul 16 19:35:27 2016 +0200
@@ -234,7 +234,7 @@
 
 ML \<open>
   fun make_benchmark n =
-    writeln (Active.sendback_markup [Markup.padding_command]
+    writeln (Active.sendback_markup_command
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 \<close>