diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Tutorial/Trie/Trie.thy
--- a/src/Doc/Tutorial/Trie/Trie.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/Trie/Trie.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -208,7 +208,7 @@
 
 
 (* Exercise 3. Solution by Getrud Bauer *)
-datatype ('a,'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option";
+datatype ('a,dead 'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option";
 
 primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
 "valuem (Triem ov m) = ov"