src/HOL/Library/Mapping.thy

 
 subsection {* Code generator setup *}
 
 code_datatype empty update
 
-instantiation mapping :: (type, type) eq
+instantiation mapping :: (type, type) equal
 begin
 
 definition [code del]:
-  "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
+  "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
 
 instance proof
-qed (simp add: eq_mapping_def)
+qed (simp add: equal_mapping_def)
 
 end
 
 
 hide_const (open) empty is_empty lookup update delete ordered_keys keys size