can now deal with type variables in nominal datatype definitions
theory Classicalimports "../NewParser"begin(* example from my Urban's PhD *)atom_decl nameatom_decl conamedeclare [[STEPS = 9]]nominal_datatype trm = Ax "name" "coname"| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2| AndL1 n::"name" t::"trm" "name" bind n in t| AndL2 n::"name" t::"trm" "name" bind n in t| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in tthm alpha_trm_raw.intros[no_vars](*thm trm.fvthm trm.eq_iffthm trm.bnthm trm.permthm trm.inductthm trm.distinctthm trm.fv[simplified trm.supp]*)end