--- a/QuotMain.thy	Mon Nov 23 21:48:44 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 21:59:57 2009 +0100
@@ -1162,7 +1162,7 @@
               #rel qinfo
             end
       | _ => HOLogic.eq_const dummyT 
-           (* FIXME: do the types correspond to each other? *)
+             (* FIXME: check that the types correspond to each other? *)
 end
 *}
 
@@ -1187,7 +1187,7 @@
 ML {*
 (* - applies f to the subterm of an abstraction,   *)
 (*   otherwise to the given term,                  *)
-(* - used by REGUKARIZE, therefore abstracted      *)
+(* - used by REGULARIZE, therefore abstracted      *)
 (*   variables do not have to be treated specially *)
 
 fun apply_subt f trm1 trm2 =
@@ -1257,7 +1257,8 @@
          then Const (@{const_name "Ex"}, ty) $ subtrm
          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
-    (* FIXME: should be replaced when fully applied? then 2nd argument *)
+    (* FIXME: Should = only be replaced, when fully applied? *) 
+    (* Then there must be a 2nd argument                     *)
   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
        let
          val subtrm = REGULARIZE_trm lthy t t'