# HG changeset patch
# User wenzelm
# Date 1637700225 -3600
# Node ID f0e0fc82b0b94c5c4671e5f6d582d5507ee7c00a
# Parent  a97ec0954c50b795659a02f45c410e1742095618
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;

diff -r a97ec0954c50 -r f0e0fc82b0b9 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 23 21:02:13 2021 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 23 21:43:45 2021 +0100
@@ -5,10 +5,8 @@
 section \<open>Some examples with text cartouches\<close>
 
 theory Cartouche_Examples
-imports Main
-keywords
-  "cartouche" :: diag and
-  "text_cartouche" :: thy_decl
+  imports Main
+  keywords "cartouche" :: diag
 begin
 
 subsection \<open>Regular outer syntax\<close>
@@ -135,14 +133,7 @@
 
 subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close>
 
-ML \<open>
-  Outer_Syntax.command
-    \<^command_keyword>\<open>text_cartouche\<close> ""
-    (Parse.opt_target -- Parse.input Parse.cartouche
-      >> Document_Output.document_output_markdown)
-\<close>
-
-text_cartouche
+text
 \<open>
   \<^ML>\<open>
       (