diff -r 8cf5c3e58889 -r 8ed62410236e Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Fri Nov 05 15:21:10 2010 +0000 +++ b/Nominal/Ex/TypeVarsTest.thy Sat Nov 06 06:18:41 2010 +0000 @@ -8,6 +8,7 @@ class s1 class s2 +(* FIXME nominal_datatype ('a, 'b) lam = Var "name" | App "('a::s1, 'b::s2) lam" "('a, 'b) lam" @@ -22,7 +23,7 @@ thm lam.eq_iff thm lam.fv_bn_eqvt thm lam.size_eqvt - +*) end