# HG changeset patch
# User wenzelm
# Date 1546788472 -3600
# Node ID 10644973cddef9b89b9b3c941891e71b7453e093
# Parent  1d2d4ae9ab817cf53d9a75d4784ec561a715954e
proper example for inner syntax, not name;

diff -r 1d2d4ae9ab81 -r 10644973cdde src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Jan 06 16:07:18 2019 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Jan 06 16:27:52 2019 +0100
@@ -721,8 +721,8 @@
     \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax
     (types, terms, etc.)~to use cartouches, instead of double-quoted strings
     or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
-    x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>fix x\<close>''
-    is replaced by ``\<^theory_text>\<open>fix \<open>x\<close>\<close>''.
+    x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>assume
+    A\<close>'' is replaced by ``\<^theory_text>\<open>assume \<open>A\<close>\<close>''.
 
     \<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to
     use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\<open>(infixl