equal
deleted
inserted
replaced
28 fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T = |
28 fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T = |
29 (ref (Typtab.merge (K true) (typs1, typs2)), |
29 (ref (Typtab.merge (K true) (typs1, typs2)), |
30 ref (Termtab.merge (K true) (terms1, terms2))); |
30 ref (Termtab.merge (K true) (terms1, terms2))); |
31 ); |
31 ); |
32 |
32 |
33 val _ = Context.>> CompressData.init; |
33 val _ = Context.>> (Context.map_theory CompressData.init); |
34 |
34 |
35 |
35 |
36 (* compress types *) |
36 (* compress types *) |
37 |
37 |
38 fun typ thy = |
38 fun typ thy = |