--- a/LFex.thy	Fri Nov 06 19:26:32 2009 +0100
+++ b/LFex.thy	Fri Nov 06 19:43:09 2009 +0100
@@ -159,7 +159,6 @@
 thm FV_trm_def
 
 (* FIXME: does not work yet *)
-(*
 overloading
     perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"   (unchecked)
     perm_ty   \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"       (unchecked)
@@ -169,7 +168,19 @@
 quotient_def 
   perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
 where
-  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> KIND \<Rightarrow> KIND)"
+  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
+
+quotient_def 
+  perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
+where
+  "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
+
+quotient_def 
+  perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+where
+  "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
+
 end
-*)
+
 
+