# HG changeset patch
# User wenzelm
# Date 1637684095 -3600
# Node ID 8d7d082c16495de1fba7e1dd4ab80c7e56d05a16
# Parent  fe9e590ae52f56c643ffcf43eb6be72437e1a807
clarified modules (see c299abcf7081);

diff -r fe9e590ae52f -r 8d7d082c1649 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 23 16:06:09 2021 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 23 17:14:55 2021 +0100
@@ -139,7 +139,7 @@
   Outer_Syntax.command
     \<^command_keyword>\<open>text_cartouche\<close> ""
     (Parse.opt_target -- Parse.input Parse.cartouche
-      >> Pure_Syn.document_command {markdown = true})
+      >> Document_Output.document_output_markdown)
 \<close>
 
 text_cartouche