diff -r aa452130ae7f -r d67240113f68 quotient_def.ML
--- a/quotient_def.ML	Wed Nov 25 15:43:12 2009 +0100
+++ b/quotient_def.ML	Wed Nov 25 21:48:32 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