27 sig |
27 sig |
28 structure TFrees: INST_TABLE |
28 structure TFrees: INST_TABLE |
29 structure TVars: INST_TABLE |
29 structure TVars: INST_TABLE |
30 structure Frees: INST_TABLE |
30 structure Frees: INST_TABLE |
31 structure Vars: INST_TABLE |
31 structure Vars: INST_TABLE |
|
32 val add_tfreesT: typ -> TFrees.set -> TFrees.set |
|
33 val add_tfrees: term -> TFrees.set -> TFrees.set |
|
34 val add_tvarsT: typ -> TVars.set -> TVars.set |
|
35 val add_tvars: term -> TVars.set -> TVars.set |
|
36 val add_frees: term -> Frees.set -> Frees.set |
|
37 val add_vars: term -> Vars.set -> Vars.set |
|
38 val add_tfree_namesT: typ -> Symtab.set -> Symtab.set |
|
39 val add_tfree_names: term -> Symtab.set -> Symtab.set |
|
40 val add_free_names: term -> Symtab.set -> Symtab.set |
32 val map_atypsT_same: typ Same.operation -> typ Same.operation |
41 val map_atypsT_same: typ Same.operation -> typ Same.operation |
33 val map_types_same: typ Same.operation -> term Same.operation |
42 val map_types_same: typ Same.operation -> term Same.operation |
34 val map_aterms_same: term Same.operation -> term Same.operation |
43 val map_aterms_same: term Same.operation -> term Same.operation |
35 val generalizeT_same: Symtab.set -> int -> typ Same.operation |
44 val generalizeT_same: Symtab.set -> int -> typ Same.operation |
36 val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation |
45 val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation |
75 structure Vars = Inst_Table( |
84 structure Vars = Inst_Table( |
76 type key = indexname * typ |
85 type key = indexname * typ |
77 val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord) |
86 val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord) |
78 ); |
87 ); |
79 |
88 |
|
89 val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I); |
|
90 val add_tfrees = fold_types add_tfreesT; |
|
91 val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I); |
|
92 val add_tvars = fold_types add_tvarsT; |
|
93 val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I); |
|
94 val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I); |
|
95 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I); |
|
96 val add_tfree_names = fold_types add_tfree_namesT; |
|
97 val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I); |
|
98 |
80 |
99 |
81 (* generic mapping *) |
100 (* generic mapping *) |
82 |
101 |
83 fun map_atypsT_same f = |
102 fun map_atypsT_same f = |
84 let |
103 let |