equal
deleted
inserted
replaced
127 in |
127 in |
128 map_types (Envir.norm_type subst) t $ u |
128 map_types (Envir.norm_type subst) t $ u |
129 end; |
129 end; |
130 |
130 |
131 fun head_conv cv ct = |
131 fun head_conv cv ct = |
132 if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct; |
132 if can Thm.dest_fun ct then Conv.fun_conv (head_conv cv) ct else cv ct; |
133 |
133 |
134 |
134 |
135 (*** currying transformation ***) |
135 (*** currying transformation ***) |
136 |
136 |
137 fun curry_const (A, B, C) = |
137 fun curry_const (A, B, C) = |