--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:45:06 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 13:00:07 2010 +0100
@@ -758,5 +758,40 @@
   lts = rlts / alphalts
   by (auto intro: alpha5_equivps)
 
+quotient_definition
+  "Vr5 :: name \<Rightarrow> trm5"
+as
+  "rVr5"
+
+quotient_definition
+  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
+as
+  "rAp5"
+
+quotient_definition
+  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
+as
+  "rLt5"
+
+quotient_definition
+  "Lnil :: lts"
+as
+  "rLnil"
+
+quotient_definition
+  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
+as
+  "rLcons"
+
+quotient_definition
+   "fv_trm5 :: trm5 \<Rightarrow> atom set"
+as
+  "rfv_trm5"
+
+quotient_definition
+   "fv_ltr :: lts \<Rightarrow> atom set"
+as
+  "rfv_lts"
+
 
 end