--- a/QuotMain.thy	Sat Nov 21 11:16:48 2009 +0100
+++ b/QuotMain.thy	Sat Nov 21 13:14:35 2009 +0100
@@ -1282,7 +1282,7 @@
        in     
          if ty = ty'
          then Abs (x, ty, subtrm)
-         else  mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
@@ -1392,6 +1392,7 @@
 *}
 
 ML {*
+(* FIXME: change rel_refl rel_eqv *)
 fun REGULARIZE_tac' lthy rel_refl rel_eqv =
    (REPEAT1 o FIRST1) 
      [(K (print_tac "start")) THEN' (K no_tac),