src/HOL/Tools/Nitpick/nitpick.ML
changeset 52202 d5c80b12a1f2
parent 52031 9a9238342963
child 52643 34c29356930e
equal deleted inserted replaced
52201:9fcceb3c85ae 52202:d5c80b12a1f2
   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