equal
deleted
inserted
replaced
272 case distinct (op =) consts of |
272 case distinct (op =) consts of |
273 [n] => n |
273 [n] => n |
274 | [] => fixrec_err "no defining equations for function" |
274 | [] => fixrec_err "no defining equations for function" |
275 | _ => fixrec_err "all equations in block must define the same function" |
275 | _ => fixrec_err "all equations in block must define the same function" |
276 val vars = |
276 val vars = |
277 case distinct (op = o pairself length) (map fst matchers) of |
277 case distinct (op = o apply2 length) (map fst matchers) of |
278 [vars] => vars |
278 [vars] => vars |
279 | _ => fixrec_err "all equations in block must have the same arity" |
279 | _ => fixrec_err "all equations in block must have the same arity" |
280 (* rename so all matchers use same free variables *) |
280 (* rename so all matchers use same free variables *) |
281 fun rename (vs, t) = Term.subst_free (filter_out (op =) (vs ~~ vars)) t |
281 fun rename (vs, t) = Term.subst_free (filter_out (op =) (vs ~~ vars)) t |
282 val rhs = big_lambdas vars (mk_run (foldr1 mk_mplus (map rename matchers))) |
282 val rhs = big_lambdas vars (mk_run (foldr1 mk_mplus (map rename matchers))) |