equal
deleted
inserted
replaced
53 repF is for constants' arguments; absF is for constants; |
53 repF is for constants' arguments; absF is for constants; |
54 function types need to be treated specially, since repF and absF |
54 function types need to be treated specially, since repF and absF |
55 change *) |
55 change *) |
56 |
56 |
57 fun get_fun flag lthy (rty, qty) = |
57 fun get_fun flag lthy (rty, qty) = |
|
58 if rty = qty then mk_identity qty else |
58 case (rty, qty) of |
59 case (rty, qty) of |
59 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
60 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
60 let |
61 let |
61 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
62 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
62 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
63 val fs_ty2 = get_fun flag lthy (ty2, ty2') |