src/HOL/Statespace/StateSpaceEx.thy

--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 20:53:22 2013 +0200
@@ -235,7 +235,7 @@
 
 ML {*
   fun make_benchmark n =
-    writeln (Active.sendback_markup
+    writeln (Active.sendback_markup []
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 *}