# HG changeset patch
# User urbanc
# Date 1178211628 -7200
# Node ID 6a16085eaaa1f3d0cbb2e56d2026d3e660a9aac8
# Parent  18f4014e1259e024c468d93de374667cb3812380
deleted some unnecessary type-annotations

diff -r 18f4014e1259 -r 6a16085eaaa1 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Thu May 03 17:54:36 2007 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Thu May 03 19:00:28 2007 +0200
@@ -67,9 +67,6 @@
 
 lemma subst_eqvt[eqvt]:
   fixes pi:: "name prm"
-  and   t1:: "lam"
-  and   t2:: "lam"
-  and   a :: "name"
   shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
 apply(nominal_induct t1 avoiding: b t2 rule: lam.induct)
 apply(auto simp add: perm_bij fresh_prod fresh_atm fresh_bij)
@@ -95,8 +92,6 @@
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"name prm"
-  and   \<theta>::"(name\<times>lam) list"
-  and   x::"name"
   shows "pi\<bullet>(lookup \<theta> x) = lookup (pi\<bullet>\<theta>) (pi\<bullet>x)"
 by (induct \<theta>) (auto simp add: perm_bij)