src/HOL/Library/AList.thy

--- a/src/HOL/Library/AList.thy	Thu Apr 09 15:54:09 2015 +0200
+++ b/src/HOL/Library/AList.thy	Thu Apr 09 20:42:32 2015 +0200
@@ -20,7 +20,7 @@
 
 subsection {* @{text update} and @{text updates} *}
 
-restricted primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "update k v [] = [(k, v)]"
 | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
@@ -86,7 +86,7 @@
   "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
   by (simp add: update_conv')
 
-restricted definition
+qualified definition
     updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "updates ks vs = fold (case_prod update) (zip ks vs)"
 
@@ -165,7 +165,7 @@
 
 subsection {* @{text delete} *}
 
-restricted definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
 
 lemma delete_simps [simp]:
@@ -217,7 +217,7 @@
 
 subsection {* @{text restrict} *}
 
-restricted definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
 
 lemma restr_simps [simp]:
@@ -301,7 +301,7 @@
 
 subsection {* @{text clearjunk} *}
 
-restricted function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "clearjunk [] = []"
 | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
@@ -411,7 +411,7 @@
 
 subsection {* @{text merge} *}
 
-restricted definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
 
 lemma merge_simps [simp]:
@@ -479,7 +479,7 @@
 
 subsection {* @{text compose} *}
 
-restricted function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
+qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
 where
   "compose [] ys = []"
 | "compose (x # xs) ys =
@@ -644,7 +644,7 @@
 
 subsection {* @{text map_entry} *}
 
-restricted fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "map_entry k f [] = []"
 | "map_entry k f (p # ps) =