--- a/Quot/quotient_term.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -10,31 +10,32 @@
 (*
 Regularizing an rtrm means:
  
- - Quantifiers over a type that need lifting are replaced 
+ - Quantifiers over types that need lifting are replaced 
    by bounded quantifiers, for example:
 
-      All P  ===> All (Respects R) P
+      All P  ----> All (Respects R) P
 
-   where the relation R is given by the rty and qty;
+   where the aggregate relation R is given by the rty and qty;
  
- - Abstractions over a type that needs lifting are replaced
-   by bounded abstractions:
+ - Abstractions over types that need lifting are replaced
+   by bounded abstractions, for example:
       
-      %x. P  ===> Ball (Respects R) %x. P
+      %x. P  ----> Ball (Respects R) %x. P
 
- - Equalities over the type being lifted are replaced by
-   corresponding equivalence relations:
+ - Equalities over types that need lifting are replaced by
+   corresponding equivalence relations, for example:
 
-      A = B  ===> R A B
+      A = B  ----> R A B
 
    or 
 
-      A = B  ===> (R ===> R) A B
+      A = B  ----> (R ===> R) A B
  
    for more complicated types of A and B
 *)
 
-(* builds the relation that is the argument of respects *)
+(* builds the aggregate equivalence relation *)
+(* that will be the argument of Respects     *)
 fun mk_resp_arg lthy (rty, qty) =
 let
   val thy = ProofContext.theory_of lthy
@@ -46,8 +47,9 @@
       (Type (s, tys), Type (s', tys')) =>
        if s = s' 
        then let
-              val SOME map_info = maps_lookup thy s
-              (* FIXME dont return an option, raise an exception *)
+              val map_info = maps_lookup thy s
+                             handle NotFound => 
+                               raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
               val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
               list_comb (Const (#relfun map_info, dummyT), args) 
@@ -88,7 +90,7 @@
 
 (* produces a regularized version of rtrm       *)
 (*                                              *)
-(* - the result is still contains dummyT        *)
+(* - the result still contains dummyTs          *)
 (*                                              *)
 (* - for regularisation we do not need any      *)
 (*   special treatment of bound variables       *)
@@ -124,14 +126,14 @@
          if ty = ty' then rtrm
          else mk_resp_arg lthy (domain_type ty, domain_type ty') 
 
-  | (* in this case we check whether the given equivalence relation is correct *) 
+  | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
          val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
          val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
        in 
-         if rel' = rel then rtrm else raise exc
+         if rel' aconv rel then rtrm else raise exc
        end  
 
   | (_, Const _) =>
@@ -168,10 +170,6 @@
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
 
-  | (Free (x, ty), Free (x', ty')) => 
-       (* this case cannot arrise as we start with two fully atomized terms *)
-       raise (LIFT_MATCH "regularize (frees)")
-
   | (Bound i, Bound i') =>
        if i = i' then rtrm 
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
@@ -187,32 +185,31 @@
 
 
 (*
-Injecting of Rep/Abs means:
+Injection of Rep/Abs means:
 
   For abstractions
 :
-  * If the type of the abstraction doesn't need lifting we recurse.
-
-  * If it needs lifting then we add Rep/Abs around the whole term and 
-    check if the bound variable needs lifting.
+  * If the type of the abstraction needs lifting, then we add Rep/Abs 
+    around the abstraction; otherwise we leave it unchanged.
  
-    * If it does we recurse and put Rep/Abs around all occurences
-      of the variable in the obtained subterm. This in combination
-      with the Rep/Abs from above will let us change the type of 
-      the abstraction with rewriting.
-  
   For applications:
   
-  * If the term is Respects applied to anything we leave it unchanged
+  * If the application involves a bounded quantifier, we recurse on 
+    the second argument. If the application is a bounded abstraction,
+    we always put an Re/Abs around it (since bounded abstractions
+    always need lifting). Otherwise we recurse on both arguments.
 
-  * If the term needs lifting and the head is a constant that we know
-    how to lift, we put a Rep/Abs and recurse
+  For constants:
 
-  * If the term needs lifting and the head is a Free applied to subterms
-    (if it is not applied we treated it in Abs branch) then we
-    put Rep/Abs and recurse
+  * If the constant is (op =), we leave it always unchanged. 
+    Otherwise the type of the constant needs lifting, we put
+    and Rep/Abs around it. 
 
-  * Otherwise just recurse.
+  For free variables:
+
+  * We put aRep/Abs around it if the type needs lifting.
+
+  Vars case cannot occur.
 *)
 
 fun mk_repabs lthy (T, T') trm = 
@@ -269,7 +266,7 @@
         else mk_repabs lthy (rty, T') rtrm
       end   
   
-  | _ => raise (LIFT_MATCH "injection")
+  | _ => raise (LIFT_MATCH "injection (default)")
 
 end; (* structure *)