# HG changeset patch
# User huffman
# Date 1327336159 -3600
# Node ID 80dccedd6c1411dd637cda9562d310c18cea7754
# Parent  1c9a548c0402149a26983210c7b30768ed3a5df6
generalize type of List.listrel

diff -r 1c9a548c0402 -r 80dccedd6c14 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jan 23 15:23:02 2012 +0100
+++ b/src/HOL/List.thy	Mon Jan 23 17:29:19 2012 +0100
@@ -5010,8 +5010,8 @@
 subsubsection {* Lifting Relations to Lists: all elements *}
 
 inductive_set
-  listrel :: "('a * 'a)set => ('a list * 'a list)set"
-  for r :: "('a * 'a)set"
+  listrel :: "('a \<times> 'b) set \<Rightarrow> ('a list \<times> 'b list) set"
+  for r :: "('a \<times> 'b) set"
 where
     Nil:  "([],[]) \<in> listrel r"
   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
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])