--- a/QuotMain.thy	Wed Oct 21 16:13:39 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 18:30:42 2009 +0200
@@ -640,7 +640,12 @@
 ML {*
 fun apply_subt f trm =
   case trm of
-    Abs (x, T, t) => Abs (x, T, f t)
+    Abs (x, T, t) => 
+       let 
+         val (x', t') = Term.dest_abs (x, T, t)
+       in
+         Term.absfree (x', T, f t') 
+       end
   | _ => f trm
 *}
 
@@ -654,7 +659,7 @@
        let 
           val ty1 = fastype_of trm
        in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t))    
+         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) (Abs (x, T, t)))    
        end
   | Const (@{const_name "All"}, ty) $ t =>
        let 
@@ -675,6 +680,12 @@
 *}
 
 ML {*  
+  cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"} 
+     @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})
+*}
+
+ML {*  
   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
 *}