tuned
authornipkow
Wed, 16 Dec 2020 00:08:31 +0100
changeset 73152 fa364c21df15
parent 73151 d02f91543bf1
child 73163 3c8d60f1dc53
tuned
src/HOL/Data_Structures/Trie_Fun.thy
--- a/src/HOL/Data_Structures/Trie_Fun.thy	Tue Dec 15 17:22:40 2020 +0000
+++ b/src/HOL/Data_Structures/Trie_Fun.thy	Wed Dec 16 00:08:31 2020 +0100
@@ -17,12 +17,12 @@
 "isin (Nd b m) [] = b" |
 "isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
 
-fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+fun insert :: "'a list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
 "insert [] (Nd b m) = Nd True m" |
 "insert (x#xs) (Nd b m) =
    Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> empty | Some t \<Rightarrow> t))))"
 
-fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+fun delete :: "'a list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
 "delete [] (Nd b m) = Nd False m" |
 "delete (x#xs) (Nd b m) = Nd b
    (case m x of