quotient_def.ML
changeset 389 d67240113f68
parent 374 980fdf92a834
child 496 8f1bf5266ebc
--- 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