src/HOL/Statespace/StateSpaceEx.thy
changeset 52697 6fb98a20c349
parent 50450 358b6020f8b6
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 13:12:54 2013 +0200
     1.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 20:53:22 2013 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4  
     1.5  ML {*
     1.6    fun make_benchmark n =
     1.7 -    writeln (Active.sendback_markup
     1.8 +    writeln (Active.sendback_markup []
     1.9        ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
    1.10          (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
    1.11  *}