diff -r 37285ec4387d -r e9e205b904e2 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/quotient_def.ML	Mon Dec 21 22:36:31 2009 +0100
@@ -32,6 +32,11 @@
 
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
+fun mk_compose flag (trm1, trm2) = 
+  case flag of
+    absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
+  | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
+
 fun get_fun_aux lthy s fs =
 let
   val thy = ProofContext.theory_of lthy
@@ -42,7 +47,7 @@
 end
 
 fun get_const flag lthy _ qty =
-(* FIXME: check here that _ and qty are related *)
+(* FIXME: check here that the type-constructors of _ and qty are related *)
 let
   val thy = ProofContext.theory_of lthy
   val qty_name = Long_Name.base_name (fst (dest_Type qty))
@@ -68,14 +73,18 @@
      in
        get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
      end
-  | (Type (s, []), Type (s', [])) =>
+  | (Type (s, _), Type (s', [])) =>
      if s = s'
      then mk_identity qty
      else get_const flag lthy rty qty
   | (Type (s, tys), Type (s', tys')) =>
-     if s = s'
-     then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
-     else get_const flag lthy rty qty
+     let
+        val args = map (get_fun flag lthy) (tys ~~ tys')
+     in
+        if s = s'
+        then get_fun_aux lthy s args
+        else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args)
+     end
   | (TFree x, TFree x') =>
      if x = x'
      then mk_identity qty