# HG changeset patch
# User nipkow
# Date 1620765659 -7200
# Node ID 78929c029785260003aae44bd5e1d70ce6f83754
# Parent  0d79ac2eb10658094f0f7a05e748daf0873aa2ad
generalized type

diff -r 0d79ac2eb106 -r 78929c029785 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Tue May 11 18:56:33 2021 +0100
+++ b/src/HOL/Library/AList.thy	Tue May 11 22:40:59 2021 +0200
@@ -475,7 +475,7 @@
 
 subsection \<open>\<open>map_ran\<close>\<close>
 
-definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+definition map_ran :: "('key \<Rightarrow> 'val1 \<Rightarrow> 'val2) \<Rightarrow> ('key \<times> 'val1) list \<Rightarrow> ('key \<times> 'val2) list"
   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
 
 lemma map_ran_simps [simp]: