equal
deleted
inserted
replaced
494 val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns |
494 val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns |
495 val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns |
495 val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns |
496 bisim_depths mono_Ts nonmono_Ts |
496 bisim_depths mono_Ts nonmono_Ts |
497 val ranks = map rank_of_block blocks |
497 val ranks = map rank_of_block blocks |
498 val all = all_combinations_ordered_smartly (map (rpair 0) ranks) |
498 val all = all_combinations_ordered_smartly (map (rpair 0) ranks) |
499 val head = (uncurry take) (max_scopes, all) |
499 val head = take max_scopes all |
500 val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks) |
500 val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks) |
501 head |
501 head |
502 in |
502 in |
503 (length all - length head, |
503 (length all - length head, |
504 descs |> length descs <= distinct_threshold ? distinct (op =) |
504 descs |> length descs <= distinct_threshold ? distinct (op =) |