src/Doc/Tutorial/Trie/Trie.thy

 apply (case_tac[!] bs, auto);
 done
 
 
 (* 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"
 
 primrec mapping :: "('a,'v) triem \<Rightarrow> 'a \<Rightarrow> ('a, 'v) triem option" where