--- a/src/HOL/ex/Cartouche_Examples.thy Wed Dec 10 20:56:33 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Thu Dec 11 15:24:28 2014 +0100
@@ -265,7 +265,7 @@
text \<open>Input source with position information:\<close>
ML \<open>
- val s: Input.source = \<open>abc\<close>;
+ val s: Input.source = \<open>abc123def456\<close>;
writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
\<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
@@ -282,6 +282,4 @@
val thms = [a, b, c];
\<close>
-ML \<open>\<close>
-
end