diff -r 0842a38dcf01 -r a045d9021c61 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 20 01:17:22 2009 +0200
+++ b/QuotMain.thy	Tue Oct 20 09:21:18 2009 +0200
@@ -1137,7 +1137,7 @@
        let 
           val ty1 = fastype_of trm
        in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    
+         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (my_reg rel t)    
        end
   | Const (@{const_name "All"}, U) $ t =>
        let 
@@ -1153,6 +1153,7 @@
        in
          (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
        end
+  | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
   | _ => trm
 *}