equal
deleted
inserted
replaced
426 val tmp_thy = |
426 val tmp_thy = |
427 let |
427 let |
428 fun arity (vs, tbind, _, _, _) = |
428 fun arity (vs, tbind, _, _, _) = |
429 (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}) |
429 (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}) |
430 in |
430 in |
431 fold Axclass.axiomatize_arity (map arity doms) tmp_thy |
431 fold Axclass.arity_axiomatization (map arity doms) tmp_thy |
432 end |
432 end |
433 |
433 |
434 (* check bifiniteness of right-hand sides *) |
434 (* check bifiniteness of right-hand sides *) |
435 fun check_rhs (_, _, _, rhs, _) = |
435 fun check_rhs (_, _, _, rhs, _) = |
436 if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then () |
436 if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then () |