diff -r 57891245370d -r 60b5c61d3de2 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/Fv.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -137,7 +137,7 @@
 *)
 
 ML {*
-datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
+datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst;
 *}
 
 ML {*