equal
deleted
inserted
replaced
26 open BNF_LFP_Tactics |
26 open BNF_LFP_Tactics |
27 |
27 |
28 (*all BNFs have the same lives*) |
28 (*all BNFs have the same lives*) |
29 fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy = |
29 fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy = |
30 let |
30 let |
|
31 val time = time lthy; |
31 val timer = time (Timer.startRealTimer ()); |
32 val timer = time (Timer.startRealTimer ()); |
32 |
33 |
33 val live = live_of_bnf (hd bnfs); |
34 val live = live_of_bnf (hd bnfs); |
34 val n = length bnfs; (*active*) |
35 val n = length bnfs; (*active*) |
35 val ks = 1 upto n; |
36 val ks = 1 upto n; |