--- a/LamEx.thy	Fri Oct 30 15:32:04 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 15:35:42 2009 +0100
@@ -11,12 +11,6 @@
 | rApp "rlam" "rlam"
 | rLam "name" "rlam"
 
-inductive 
-  alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
-where
-  a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
-| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 function
   rfv :: "rlam \<Rightarrow> name set"
@@ -28,6 +22,13 @@
 
 termination rfv sorry 
 
+inductive 
+  alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
+| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
+| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
+
 quotient lam = rlam / alpha
 sorry