427 |
427 |
428 (* declare arities in temporary theory *) |
428 (* declare arities in temporary theory *) |
429 val tmp_thy = |
429 val tmp_thy = |
430 let |
430 let |
431 fun arity (vs, tbind, mx, _, _) = |
431 fun arity (vs, tbind, mx, _, _) = |
432 (Sign.full_name thy tbind, map the_sort vs, @{sort bifinite}); |
432 (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}); |
433 in |
433 in |
434 fold AxClass.axiomatize_arity (map arity doms) tmp_thy |
434 fold AxClass.axiomatize_arity (map arity doms) tmp_thy |
435 end; |
435 end; |
436 |
436 |
437 (* check bifiniteness of right-hand sides *) |
437 (* check bifiniteness of right-hand sides *) |
438 fun check_rhs (vs, tbind, mx, rhs, morphs) = |
438 fun check_rhs (vs, tbind, mx, rhs, morphs) = |
439 if Sign.of_sort tmp_thy (rhs, @{sort bifinite}) then () |
439 if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then () |
440 else error ("Type not of sort bifinite: " ^ |
440 else error ("Type not of sort domain: " ^ |
441 quote (Syntax.string_of_typ_global tmp_thy rhs)); |
441 quote (Syntax.string_of_typ_global tmp_thy rhs)); |
442 val _ = map check_rhs doms; |
442 val _ = map check_rhs doms; |
443 |
443 |
444 (* domain equations *) |
444 (* domain equations *) |
445 fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = |
445 fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = |