diff -r 1c9a548c0402 -r 80dccedd6c14 src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Mon Jan 23 15:23:02 2012 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Mon Jan 23 17:29:19 2012 +0100
@@ -424,6 +424,7 @@
 declare listrel_mono [mono_set]
 
 lemma listrelp_eqvt [eqvt]:
+  fixes f :: "'a::pt_name \<Rightarrow> 'b::pt_name \<Rightarrow> bool"
   assumes xy: "listrelp f (x::'a::pt_name list) y"
   shows "listrelp ((pi::name prm) \<bullet> f) (pi \<bullet> x) (pi \<bullet> y)" using xy
   by induct (simp_all add: listrelp.intros perm_app [symmetric])