--- 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>