src/Doc/Eisbach/Manual.thy

--- a/src/Doc/Eisbach/Manual.thy	Tue Dec 22 17:14:35 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Tue Dec 22 17:41:46 2015 +0100
@@ -284,7 +284,7 @@
   further defined in @{cite "isabelle-isar-ref"}.
 
   @{rail \<open>
-    @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')
+    @@{method match} kind @'in' (pattern '\<Rightarrow>' @{syntax text} + '\<bar>')
     ;
     kind:
       (@'conclusion' | @'premises' ('(' 'local' ')')? |