equal
deleted
inserted
replaced
87 val c = HOLogic.pair_const ty1 ty2 |
87 val c = HOLogic.pair_const ty1 ty2 |
88 in c $ fst $ snd |
88 in c $ fst $ snd |
89 end; |
89 end; |
90 |
90 |
91 *} |
91 *} |
|
92 |
|
93 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
92 |
94 |
93 ML {* |
95 ML {* |
94 (* Currently needs just one full_tname to access Datatype *) |
96 (* Currently needs just one full_tname to access Datatype *) |
95 fun define_fv_alpha full_tname bindsall lthy = |
97 fun define_fv_alpha full_tname bindsall lthy = |
96 let |
98 let |