equal
deleted
inserted
replaced
207 handle Subscript => error "infer_arities: bad term") |
207 handle Subscript => error "infer_arities: bad term") |
208 | _ => fold (infer_arities thy arities) (map (pair NONE) ts) |
208 | _ => fold (infer_arities thy arities) (map (pair NONE) ts) |
209 (case optf of |
209 (case optf of |
210 NONE => fs |
210 NONE => fs |
211 | SOME f => AList.update op = (u, the_default f |
211 | SOME f => AList.update op = (u, the_default f |
212 (Option.map (curry (gen_inter (op =)) f) (AList.lookup op = fs u))) fs)); |
212 (Option.map (curry (inter (op =)) f) (AList.lookup op = fs u))) fs)); |
213 |
213 |
214 |
214 |
215 (**************************************************************) |
215 (**************************************************************) |
216 (* derive the to_pred equation from the to_set equation *) |
216 (* derive the to_pred equation from the to_set equation *) |
217 (* *) |
217 (* *) |