equal
deleted
inserted
replaced
63 handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) |
63 handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) |
64 |
64 |
65 (*Add a const/type pair to the table, but a [] entry means a standard connective, |
65 (*Add a const/type pair to the table, but a [] entry means a standard connective, |
66 which we ignore.*) |
66 which we ignore.*) |
67 fun add_const_typ_table ((c,ctyps), tab) = |
67 fun add_const_typ_table ((c,ctyps), tab) = |
68 Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => ctyps ins ctyps_list) |
68 Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) |
69 tab; |
69 tab; |
70 |
70 |
71 (*Free variables are included, as well as constants, to handle locales*) |
71 (*Free variables are included, as well as constants, to handle locales*) |
72 fun add_term_consts_typs_rm thy (Const(c, typ), tab) = |
72 fun add_term_consts_typs_rm thy (Const(c, typ), tab) = |
73 add_const_typ_table (const_with_typ thy (c,typ), tab) |
73 add_const_typ_table (const_with_typ thy (c,typ), tab) |