# HG changeset patch
# User wenzelm
# Date 1546778673 -3600
# Node ID d80b2df54d31c47e5cb8ef38fb57af93d1026031
# Parent  67ae2e164c0fd2543e575e7e202462e0c46f028b
isabelle update -u control_cartouches;

diff -r 67ae2e164c0f -r d80b2df54d31 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Jan 06 12:42:26 2019 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Jan 06 13:44:33 2019 +0100
@@ -206,7 +206,7 @@
   @{thm [display] pigeonhole_slow_def}
   The program for searching for an element in an array is
   @{thm [display,eta_contract=false] search_def}
-  The correctness statement for @{term "pigeonhole"} is
+  The correctness statement for \<^term>\<open>pigeonhole\<close> is
   @{thm [display] pigeonhole_correctness [no_vars]}
 
   In order to analyze the speed of the above programs,
diff -r 67ae2e164c0f -r d80b2df54d31 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 06 12:42:26 2019 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 06 13:44:33 2019 +0100
@@ -123,11 +123,11 @@
 text \<open>
   \<^ML>\<open>
       (
-        @{term \<open>""\<close>};
-        @{term \<open>"abc"\<close>};
-        @{term \<open>"abc" @ "xyz"\<close>};
-        @{term \<open>"\<newline>"\<close>};
-        @{term \<open>"\001\010\100"\<close>}
+        \<^term>\<open>""\<close>;
+        \<^term>\<open>"abc"\<close>;
+        \<^term>\<open>"abc" @ "xyz"\<close>;
+        \<^term>\<open>"\<newline>"\<close>;
+        \<^term>\<open>"\001\010\100"\<close>
       )
     \<close>
 \<close>
@@ -146,11 +146,11 @@
 \<open>
   \<^ML>\<open>
       (
-        @{term \<open>""\<close>};
-        @{term \<open>"abc"\<close>};
-        @{term \<open>"abc" @ "xyz"\<close>};
-        @{term \<open>"\<newline>"\<close>};
-        @{term \<open>"\001\010\100"\<close>}
+        \<^term>\<open>""\<close>;
+        \<^term>\<open>"abc"\<close>;
+        \<^term>\<open>"abc" @ "xyz"\<close>;
+        \<^term>\<open>"\<newline>"\<close>;
+        \<^term>\<open>"\001\010\100"\<close>
       )
     \<close>
 \<close>