# HG changeset patch
# User wenzelm
# Date 1390400899 -3600
# Node ID 917e799f19da8e94f525b41357977f4808ecd962
# Parent  ecff9e26360cf761097cb2d5cac7418d4d63f5c6
avoid breakdown of document preparation, which does not understand cartouche tokens yet;

diff -r ecff9e26360c -r 917e799f19da src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Jan 22 15:11:10 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Jan 22 15:28:19 2014 +0100
@@ -150,7 +150,7 @@
 subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *}
 
 ML {*
-  Outer_Syntax.markup_command Thy_Output.MarkupEnv
+  Outer_Syntax.command
     @{command_spec "text_cartouche"} ""
     (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup)
 *}