diff -r e77def9a63a6 -r 63af76397a60 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Nov 13 21:28:57 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Nov 13 21:31:04 2015 +0100
@@ -316,7 +316,7 @@
 text \<open>
   Wherever explicit propositions (or term fragments) occur in a proof text,
   casual binding of schematic term variables may be given specified via
-  patterns of the form ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''. This works both for @{syntax
+  patterns of the form ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. This works both for @{syntax
   term} and @{syntax prop}.
 
   @{rail \<open>