Nominal/Ex1rec.thy
changeset 1706 e92dd76dfb03
parent 1596 c69d9fb16785
--- 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'"