# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259010054 -3600
# Node ID 28e312cfc80632d31226f841c89978da1552c8b1
# Parent  3aba0cf85f97fe5a354c21adde5a0b3e584b4892# Parent  2674bd315993382601d488ac18b2fa450b7df387
merged

diff -r 2674bd315993 -r 28e312cfc806 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 21:56:30 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 22:00:54 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'