diff -r 471308f23649 -r e92dd76dfb03 Nominal/Ex1rec.thy --- a/Nominal/Ex1rec.thy Tue Mar 30 09:15:40 2010 +0200 +++ b/Nominal/Ex1rec.thy Tue Mar 30 10:36:05 2010 +0200 @@ -5,6 +5,7 @@ atom_decl name ML {* val _ = recursive := true *} +ML {* val _ = alpha_type := AlphaGen *} nominal_datatype lam' = VAR' "name" | APP' "lam'" "lam'"