40 |
40 |
41 val deads = fold (union (op =)) Dss resDs; |
41 val deads = fold (union (op =)) Dss resDs; |
42 val names_lthy = fold Variable.declare_typ deads lthy; |
42 val names_lthy = fold Variable.declare_typ deads lthy; |
43 |
43 |
44 (* tvars *) |
44 (* tvars *) |
45 val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')), |
45 val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) = |
46 activeCs), passiveXs), passiveYs) = names_lthy |
46 names_lthy |
47 |> mk_TFrees live |
47 |> mk_TFrees m |
48 |> apfst (`(chop m)) |
48 ||>> mk_TFrees n |
49 ||> mk_TFrees live |
49 ||>> mk_TFrees m |
50 ||>> apfst (`(chop m)) |
50 ||>> mk_TFrees n |
51 ||>> mk_TFrees n |
51 ||>> mk_TFrees n |
52 ||>> mk_TFrees m |
52 ||>> mk_TFrees m |
53 ||> fst o mk_TFrees m; |
53 ||> fst o mk_TFrees m; |
54 |
54 |
|
55 val allAs = passiveAs @ activeAs; |
|
56 val allBs' = passiveBs @ activeBs; |
55 val Ass = replicate n allAs; |
57 val Ass = replicate n allAs; |
56 val allBs = passiveAs @ activeBs; |
58 val allBs = passiveAs @ activeBs; |
57 val Bss = replicate n allBs; |
59 val Bss = replicate n allBs; |
58 val allCs = passiveAs @ activeCs; |
60 val allCs = passiveAs @ activeCs; |
59 val allCs' = passiveBs @ activeCs; |
61 val allCs' = passiveBs @ activeCs; |