--- a/src/HOL/Data_Structures/Map_by_Ordered.thy Sun Jan 17 00:14:45 2016 +0100
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy Sun Jan 17 17:56:33 2016 +0100
@@ -10,11 +10,11 @@
fixes empty :: "'m"
fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
-fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
fixes invar :: "'m \<Rightarrow> bool"
-assumes map_empty: "map_of empty = (\<lambda>_. None)"
-and map_update: "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
-and map_delete: "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
+assumes map_empty: "lookup empty = (\<lambda>_. None)"
+and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
+and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup m)(a := None)"
and invar_empty: "invar empty"
and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"