src/HOL/Statespace/StateSpaceEx.thy

--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Nov 22 13:21:02 2012 +0100
@@ -235,7 +235,7 @@
 
 ML {*
   fun make_benchmark n =
-    writeln (Markup.markup Isabelle_Markup.sendback
+    writeln (Sendback.markup
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 *}