src/HOL/Statespace/StateSpaceEx.thy

--- a/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 28 22:05:32 2011 +0100
@@ -235,7 +235,7 @@
 
 ML {*
   fun make_benchmark n =
-    writeln (Markup.markup Markup.sendback
+    writeln (Markup.markup Isabelle_Markup.sendback
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 *}