equal
deleted
inserted
replaced
90 |
90 |
91 *} |
91 *} |
92 |
92 |
93 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
93 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
94 ML {* |
94 ML {* |
95 (* Currently needs just one full_tname to access Datatype *) |
95 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = |
96 fun define_fv_alpha full_tname bindsall lthy = |
|
97 let |
96 let |
98 val thy = ProofContext.theory_of lthy; |
97 val thy = ProofContext.theory_of lthy; |
99 val {descr, ...} = Datatype.the_info thy full_tname; |
98 val {descr, sorts, ...} = dt_info; |
100 val sorts = []; (* TODO *) |
|
101 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
99 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
102 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
100 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
103 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
101 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
104 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
102 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
105 val fv_frees = map Free (fv_names ~~ fv_types); |
103 val fv_frees = map Free (fv_names ~~ fv_types); |