Nominal/Ex/TypeVarsTest.thy
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