diff -r 0755f8fd56b3 -r 71225f4a4635 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Dec 31 23:53:10 2009 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 01 01:08:19 2010 +0100
@@ -40,9 +40,6 @@
 val mk_id = Const (@{const_name "id"}, dummyT)
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
-
 fun mk_compose flag (trm1, trm2) = 
   case flag of
     absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
@@ -57,10 +54,17 @@
   Const (mapfun, dummyT)
 end
 
+(* makes a Free out of a TVar *)
+fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+
 (* produces an aggregate map function for the       *)
 (* rty-part of a quotient definition; abstracts     *)
 (* over all variables listed in vs (these variables *)
 (* correspond to the type variables in rty)         *)        
+(*                                                  *)
+(* for example for: ?'a list                        *)
+(* it produces:     %a. map a                       *)
+(* 
 fun mk_mapfun ctxt vs ty =
 let
   val vs' = map (mk_Free) vs
@@ -96,7 +100,7 @@
   (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
 end
 
-(* produces the rep or abs constants for a qty *)
+(* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
 let
   val thy = ProofContext.theory_of ctxt
@@ -175,7 +179,7 @@
                           handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
              val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
                           handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty 
-             val args_aux = map (double_lookup rtyenv qtyenv) vs            
+             val args_aux = map (double_lookup rtyenv qtyenv) vs 
              val args = map (absrep_fun flag ctxt) args_aux
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args)