# HG changeset patch
# User nipkow
# Date 1608073711 -3600
# Node ID fa364c21df15df629ada23e80cbe31ffda1acffd
# Parent  d02f91543bf142aacf21f5ab2035d630ecec0784
tuned

diff -r d02f91543bf1 -r fa364c21df15 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