--- 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