equal
deleted
inserted
replaced
524 |
524 |
525 val distinct_thms = map prove_distinct_thms (dist_rewrites ~~ |
525 val distinct_thms = map prove_distinct_thms (dist_rewrites ~~ |
526 DatatypeProp.make_distincts new_type_names descr sorts thy5); |
526 DatatypeProp.make_distincts new_type_names descr sorts thy5); |
527 |
527 |
528 val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => |
528 val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => |
529 if length constrs < ConfigOption.get_thy thy5 DatatypeProp.distinctness_limit |
529 if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit |
530 then FewConstrs dists |
530 then FewConstrs dists |
531 else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~ |
531 else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~ |
532 constr_rep_thms ~~ rep_congs ~~ distinct_thms); |
532 constr_rep_thms ~~ rep_congs ~~ distinct_thms); |
533 |
533 |
534 (* prove injectivity of constructors *) |
534 (* prove injectivity of constructors *) |