# HG changeset patch
# User wenzelm
# Date 1418307868 -3600
# Node ID 580de802aafd1a7766c0314f768f790a0cb04f48
# Parent  f4b6e2626cf80ce97a788b06e557df6d8f3bcfe4
tuned;

diff -r f4b6e2626cf8 -r 580de802aafd src/HOL/ex/Cartouche_Examples.thy
--- 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