--- a/QuotMain.thy	Tue Oct 20 09:21:18 2009 +0200
+++ b/QuotMain.thy	Tue Oct 20 09:31:34 2009 +0200
@@ -1129,7 +1129,9 @@
   | _ => f trm
 *}
 
+
 (* FIXME: assumes always the typ is qty! *)
+(* FIXME: if there are more than one quotient, then you have to look up the relation *)
 ML {*
 fun my_reg rel trm =
   case trm of
@@ -1137,18 +1139,18 @@
        let 
           val ty1 = fastype_of trm
        in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (my_reg rel t)    
+         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t))    
        end
-  | Const (@{const_name "All"}, U) $ t =>
+  | Const (@{const_name "All"}, ty) $ t =>
        let 
-          val ty1 = fastype_of t
+          val ty1 = domain_type ty
           val ty2 = domain_type ty1
        in
          (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
        end
-  | Const (@{const_name "Ex"}, U) $ t =>
+  | Const (@{const_name "Ex"}, ty) $ t =>
        let 
-          val ty1 = fastype_of t
+          val ty1 = domain_type ty
           val ty2 = domain_type ty1
        in
          (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)