diff -r d16abc8f4fb0 -r 23c4a349feff doc-src/TutorialI/Trie/Trie.thy
--- a/doc-src/TutorialI/Trie/Trie.thy	Wed Sep 21 13:28:44 2005 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Wed Sep 21 14:00:28 2005 +0200
@@ -19,7 +19,7 @@
 We define two selector functions:
 *};
 
-consts value :: "('a,'v)trie \<Rightarrow> 'v option"
+consts "value" :: "('a,'v)trie \<Rightarrow> 'v option"
        alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list";
 primrec "value(Trie ov al) = ov";
 primrec "alist(Trie ov al) = al";