--- a/Nominal/NewAlpha.thy	Fri May 21 11:40:18 2010 +0100
+++ b/Nominal/NewAlpha.thy	Sat May 22 13:51:47 2010 +0100
@@ -127,7 +127,7 @@
 let
   fun mk_alphabn_free (bn, ith, _) =
     let
-      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn)));
       val ty = nth_dtyp dt_descr sorts ith;
       val alphabn_type = ty --> ty --> @{typ bool};
       val alphabn_free = Free(alphabn_name, alphabn_type);