--- a/Quot/Nominal/LFex.thy	Tue Feb 23 09:31:59 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Tue Feb 23 09:34:41 2010 +0100
@@ -18,21 +18,6 @@
   | App "trm" "trm"
   | Lam "ty" "name" "trm"
 
-primrec
-    rfv_kind :: "kind \<Rightarrow> atom set"
-and rfv_ty   :: "ty \<Rightarrow> atom set"
-and rfv_trm  :: "trm \<Rightarrow> atom set"
-where
-  "rfv_kind (Type) = {}"
-| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
-| "rfv_ty (TConst i) = {atom i}"
-| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
-| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
-| "rfv_trm (Const i) = {atom i}"
-| "rfv_trm (Var x) = {atom x}"
-| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
-| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
-
 instantiation kind and ty and trm :: pt
 begin
 
@@ -74,6 +59,21 @@
 
 end
 
+primrec
+    rfv_kind :: "kind \<Rightarrow> atom set"
+and rfv_ty   :: "ty \<Rightarrow> atom set"
+and rfv_trm  :: "trm \<Rightarrow> atom set"
+where
+  "rfv_kind (Type) = {}"
+| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
+| "rfv_ty (TConst i) = {atom i}"
+| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
+| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
+| "rfv_trm (Const i) = {atom i}"
+| "rfv_trm (Var x) = {atom x}"
+| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
+| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
+
 inductive
     akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)