diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/Fv.thy	Wed Apr 21 10:20:48 2010 +0200
@@ -137,7 +137,7 @@
 *)
 
 ML {*
-datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
+datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst;
 *}
 
 ML {*