changeset 58305 | 57752a91eec4 |
parent 48985 | 5386df44a037 |
child 58860 | fee7cfa69c50 |
--- 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"