432 val core_u = choose_reps_in_nut scope liberal rep_table false core_u |
432 val core_u = choose_reps_in_nut scope liberal rep_table false core_u |
433 val def_us = map (choose_reps_in_nut scope liberal rep_table true) |
433 val def_us = map (choose_reps_in_nut scope liberal rep_table true) |
434 def_us |
434 def_us |
435 val nondef_us = map (choose_reps_in_nut scope liberal rep_table false) |
435 val nondef_us = map (choose_reps_in_nut scope liberal rep_table false) |
436 nondef_us |
436 nondef_us |
437 (* |
437 (*### |
|
438 *) |
438 val _ = List.app (priority o string_for_nut ctxt) |
439 val _ = List.app (priority o string_for_nut ctxt) |
439 (free_names @ sel_names @ nonsel_names @ |
440 (free_names @ sel_names @ nonsel_names @ |
440 core_u :: def_us @ nondef_us) |
441 core_u :: def_us @ nondef_us) |
441 *) |
|
442 val (free_rels, pool, rel_table) = |
442 val (free_rels, pool, rel_table) = |
443 rename_free_vars free_names initial_pool NameTable.empty |
443 rename_free_vars free_names initial_pool NameTable.empty |
444 val (sel_rels, pool, rel_table) = |
444 val (sel_rels, pool, rel_table) = |
445 rename_free_vars sel_names pool rel_table |
445 rename_free_vars sel_names pool rel_table |
446 val (other_rels, pool, rel_table) = |
446 val (other_rels, pool, rel_table) = |