equal
deleted
inserted
replaced
542 if n' > n then (nickname_of name, n') else (s, n) |
542 if n' > n then (nickname_of name, n') else (s, n) |
543 end) rep_table ("", 1) |
543 end) rep_table ("", 1) |
544 val min_univ_card = |
544 val min_univ_card = |
545 NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table |
545 NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table |
546 (univ_card nat_card int_card main_j0 [] KK.True) |
546 (univ_card nat_card int_card main_j0 [] KK.True) |
547 val _ = if debug then () |
547 val _ = check_arity guiltiest_party min_univ_card min_highest_arity |
548 else check_arity guiltiest_party min_univ_card min_highest_arity |
|
549 |
548 |
550 val def_us = |
549 val def_us = |
551 def_us |> map (choose_reps_in_nut scope unsound rep_table true) |
550 def_us |> map (choose_reps_in_nut scope unsound rep_table true) |
552 val nondef_us = |
551 val nondef_us = |
553 nondef_us |> map (choose_reps_in_nut scope unsound rep_table false) |
552 nondef_us |> map (choose_reps_in_nut scope unsound rep_table false) |
610 val axioms = built_in_axioms @ declarative_axioms |
609 val axioms = built_in_axioms @ declarative_axioms |
611 val highest_arity = |
610 val highest_arity = |
612 fold Integer.max (map (fst o fst) (maps fst bounds)) 0 |
611 fold Integer.max (map (fst o fst) (maps fst bounds)) 0 |
613 val formula = fold_rev s_and axioms formula |
612 val formula = fold_rev s_and axioms formula |
614 val _ = if bits = 0 then () else check_bits bits formula |
613 val _ = if bits = 0 then () else check_bits bits formula |
615 val _ = if debug orelse formula = KK.False then () |
614 val _ = if formula = KK.False then () |
616 else check_arity "" univ_card highest_arity |
615 else check_arity "" univ_card highest_arity |
617 in |
616 in |
618 SOME ({comment = comment, settings = settings, univ_card = univ_card, |
617 SOME ({comment = comment, settings = settings, univ_card = univ_card, |
619 tuple_assigns = [], bounds = bounds, |
618 tuple_assigns = [], bounds = bounds, |
620 int_bounds = if bits = 0 then sequential_int_bounds univ_card |
619 int_bounds = if bits = 0 then sequential_int_bounds univ_card |