changeset 2888 | eda5aeb056a6 |
parent 2730 | eebc24b9cf39 |
child 2950 | 0911cb7bf696 |
--- a/Nominal/Ex/TypeVarsTest.thy Wed Jun 22 14:14:54 2011 +0100 +++ b/Nominal/Ex/TypeVarsTest.thy Thu Jun 23 11:30:39 2011 +0100 @@ -38,11 +38,10 @@ thm lam.fv_bn_eqvt thm lam.size_eqvt -(* FIXME: only works for type variables 'a 'b 'c *) -nominal_datatype ('a, 'b, 'c) psi = +nominal_datatype ('alpha, 'beta, 'gamma) psi = PsiNil -| Output "'a" "'a" "('a, 'b, 'c) psi" +| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" end