--- a/QuotMain.thy	Sat Nov 21 23:23:01 2009 +0100
+++ b/QuotMain.thy	Sun Nov 22 00:01:06 2009 +0100
@@ -1206,6 +1206,8 @@
 (******************************************)
 
 ML {*
+(* builds the relation for respects *)
+ 
 fun mk_resp_arg lthy (rty, qty) =
 let
   val thy = ProofContext.theory_of lthy
@@ -1221,10 +1223,13 @@
             end  
        else let  
               val SOME qinfo = quotdata_lookup_thy thy s'
+              (* FIXME: check in this case that the rty and qty *)
+              (* FIXME: correspond to each other *)
             in
               #rel qinfo
             end
-    | _ => HOLogic.eq_const dummyT
+    | _ => HOLogic.eq_const dummyT 
+           (* FIXME: do the types correspond to each other? *)
 end
 *}
 
@@ -1247,33 +1252,46 @@
 *}
 
 ML {*
-(* applies f to the subterm of an abstractions, otherwise to the given term *)
-(* abstracted variables do not have to be treated specially *)
+(* - applies f to the subterm of an abstraction,   *)
+(*   otherwise to the given term,                  *)
+(* - used by REGUKARIZE, therefore abstracted      *)
+(*   variables do not have to be treated specially *)
+
 fun apply_subt f trm1 trm2 =
   case (trm1, trm2) of
     (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
   | _ => f trm1 trm2
 
+(* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)
 *}
 
 (*
-Regularizing an rterm means:
- - Quantifiers over a type that needs lifting are replaced by
+Regularizing an rtrm means:
+ - quantifiers over a type that needs lifting are replaced by
    bounded quantifiers, for example:
-      \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
- - Abstractions over a type that needs lifting are replaced
+      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
+
+   the relation R is given by the rty and qty;
+ 
+ - abstractions over a type that needs lifting are replaced
    by bounded abstractions:
       \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
 
- - Equalities over the type being lifted are replaced by
-   appropriate relations:
+ - equalities over the type being lifted are replaced by
+   corresponding relations:
       A = B     \<Longrightarrow>     A \<approx> B
-   Example with more complicated types of A, B:
+
+   example with more complicated types of A, B:
       A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
 *)
 
 ML {*
+(* produces a regularized version of rtm      *)
+(* - the result is still not completely typed *)
+(* - does not need any special treatment of   *)
+(*   bound variables                          *)
+
 fun REGULARIZE_trm lthy rtrm qtrm =
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (x', ty', t')) =>
@@ -1313,7 +1331,7 @@
        (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
   | (Free (x, ty), Free (x', ty')) =>
        if x = x' 
-       then rtrm 
+       then rtrm     (* FIXME: check whether types corresponds *)
        else trm_lift_error lthy rtrm qtrm
   | (Bound i, Bound i') =>
        if i = i' 
@@ -1328,12 +1346,13 @@
 
 ML {*
 fun mk_REGULARIZE_goal lthy rtrm qtrm =
-      Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy)
+  Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
 *}
 
 (*
 To prove that the old theorem implies the new one, we first
 atomize it and then try:
+
  - Reflexivity of the relation
  - Assumption
  - Elimnating quantifiers on both sides of toplevel implication
@@ -1362,6 +1381,7 @@
 done
 
 ML {*
+(* FIXME: get_rid of rel_refl rel_eqv *)
 fun REGULARIZE_tac lthy rel_refl rel_eqv =
    (REPEAT1 o FIRST1) 
      [rtac rel_refl,
@@ -1376,7 +1396,7 @@
       rtac @{thm RIGHT_RES_FORALL_REGULAR}]
 *}
 
-(* same version including debugging information *)
+(* version of REGULARIZE_tac including debugging information *)
 ML {*
 fun my_print_tac ctxt s thm =
 let
@@ -1392,7 +1412,6 @@
 *}
 
 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), 
@@ -1412,10 +1431,9 @@
 fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
   let
     val goal = mk_REGULARIZE_goal lthy rtrm qtrm
-    val cthm = Goal.prove lthy [] [] goal 
+  in
+    Goal.prove lthy [] [] goal 
       (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
-  in
-    cthm 
   end
 *}