# HG changeset patch
# User wenzelm
# Date 1515453383 -3600
# Node ID 39e4668ded4f1b593121ac63da0d284507989f5c
# Parent  146757999c8da0867702c5c684649cd9a4819f39
updated to 146757999c8d;

diff -r 146757999c8d -r 39e4668ded4f src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Mon Jan 08 23:45:43 2018 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Jan 09 00:16:23 2018 +0100
@@ -141,7 +141,7 @@
   Outer_Syntax.command
     @{command_keyword text_cartouche} ""
     (Parse.opt_target -- Parse.input Parse.cartouche
-      >> Thy_Output.document_command {markdown = true})
+      >> Pure_Syn.document_command {markdown = true})
 \<close>
 
 text_cartouche