diff -r c8a2755bf220 -r ff784d5a5bfb src/Doc/Tutorial/Rules/Basic.thy
--- a/src/Doc/Tutorial/Rules/Basic.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Tutorial/Rules/Basic.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -371,7 +371,7 @@
 @{subgoals[display,indent=0,margin=65]}
 
 applying @text{someI} automatically instantiates
-@{term f} to @{term "\<lambda>x. SOME y. P x y"}
+\<^term>\<open>f\<close> to \<^term>\<open>\<lambda>x. SOME y. P x y\<close>
 \<close>
 
 by (rule someI)