--- a/quotient_def.ML	Thu Nov 26 02:31:00 2009 +0100
+++ b/quotient_def.ML	Thu Nov 26 03:18:38 2009 +0100
@@ -55,6 +55,7 @@
    change *)
 
 fun get_fun flag lthy (rty, qty) =
+  if rty = qty then mk_identity qty else
   case (rty, qty) of 
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
      let