diff -r 27a643e00675 -r 6f6ee78c7357 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 01 04:39:43 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 01 11:30:00 2010 +0100
@@ -37,7 +37,6 @@
 fun negF absF = repF
   | negF repF = absF
 
-val mk_id = Const (@{const_name "id"}, dummyT)
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
 fun mk_compose flag (trm1, trm2) = 
@@ -62,20 +61,20 @@
 (* 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 =
+(* for example for: (?'a list * ?'b)                *)
+(* it produces:     %a b. prod_map (map a) b        *)
+fun mk_mapfun ctxt vs rty =
 let
   val vs' = map (mk_Free) vs
 
-  fun mk_mapfun_aux ty =
-    case ty of
-      TVar _ => mk_Free ty
-    | Type (_, []) => mk_id
+  fun mk_mapfun_aux rty =
+    case rty of
+      TVar _ => mk_Free rty
+    | Type (_, []) => mk_identity rty
     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
     | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)")
 in
-  fold_rev Term.lambda vs' (mk_mapfun_aux ty)
+  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
 
 (* looks up the (varified) rty and qty for *)
@@ -121,6 +120,8 @@
 
 (* produces an aggregate absrep function                           *)
 (*                                                                 *)
+(* - In case of equal types we just return the identity            *)
+(*                                                                 *)
 (* - In case of function types and TFrees, we recurse, taking in   *) 
 (*   the first case the polarity change into account.              *)
 (*                                                                 *)
@@ -152,7 +153,7 @@
 
 fun absrep_fun flag ctxt (rty, qty) =
   if rty = qty  
-  then mk_identity qty
+  then mk_identity rty
   else
     case (rty, qty) of
       (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
@@ -187,7 +188,7 @@
            end 
     | (TFree x, TFree x') =>
         if x = x'
-        then mk_identity qty
+        then mk_identity rty
         else raise (LIFT_MATCH "absrep_fun (frees)")
     | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
     | _ => raise (LIFT_MATCH "absrep_fun (default)")