equal
deleted
inserted
replaced
55 ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; |
55 ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; |
56 |
56 |
57 (*all BNFs have the same lives*) |
57 (*all BNFs have the same lives*) |
58 fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy = |
58 fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy = |
59 let |
59 let |
|
60 val time = time lthy; |
60 val timer = time (Timer.startRealTimer ()); |
61 val timer = time (Timer.startRealTimer ()); |
61 |
62 |
62 val live = live_of_bnf (hd bnfs); |
63 val live = live_of_bnf (hd bnfs); |
63 val n = length bnfs; (*active*) |
64 val n = length bnfs; (*active*) |
64 val ks = 1 upto n; |
65 val ks = 1 upto n; |