equal
deleted
inserted
replaced
52 open BNF_Def |
52 open BNF_Def |
53 open BNF_Util |
53 open BNF_Util |
54 open BNF_Tactics |
54 open BNF_Tactics |
55 open BNF_Comp_Tactics |
55 open BNF_Comp_Tactics |
56 |
56 |
57 val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID"); |
57 val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID"); |
58 val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID"); |
58 val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID"); |
59 |
59 |
60 type comp_cache = (bnf * (typ list * typ list)) Typtab.table; |
60 type comp_cache = (bnf * (typ list * typ list)) Typtab.table; |
61 |
61 |
62 fun key_of_types s Ts = Type (s, Ts); |
62 fun key_of_types s Ts = Type (s, Ts); |
63 fun key_of_typess s = key_of_types s o map (key_of_types ""); |
63 fun key_of_typess s = key_of_types s o map (key_of_types ""); |