Index: kernel/arch/ia32xen/src/smp/mps.c
===================================================================
--- kernel/arch/ia32xen/src/smp/mps.c	(revision 566f5e5c2e933d72fd5d40b30c7da09eb035d5ea)
+++ kernel/arch/ia32xen/src/smp/mps.c	(revision 6b781c0c856d94b3114ccd6375bc6667a19e9bfe)
@@ -195,5 +195,5 @@
 	if (fs->config_type == 0 && fs->configuration_table) {
 		if (fs->mpfib2 >> 7) {
-			printf("%s: PIC mode not supported\n", __FUNCTION__);
+			printf("%s: PIC mode not supported\n", __func__);
 			return;
 		}
@@ -214,13 +214,13 @@
 		
 	if (ct->signature != CT_SIGNATURE) {
-		printf("%s: bad ct->signature\n", __FUNCTION__);
+		printf("%s: bad ct->signature\n", __func__);
 		return 1;
 	}
 	if (!mps_ct_check()) {
-		printf("%s: bad ct checksum\n", __FUNCTION__);
+		printf("%s: bad ct checksum\n", __func__);
 		return 1;
 	}
 	if (ct->oem_table) {
-		printf("%s: ct->oem_table not supported\n", __FUNCTION__);
+		printf("%s: ct->oem_table not supported\n", __func__);
 		return 1;
 	}
@@ -277,5 +277,5 @@
 				 */
 				 
-				printf("%s: ct badness\n", __FUNCTION__);
+				printf("%s: ct badness\n", __func__);
 				return 1;
 		}
@@ -294,5 +294,5 @@
 	 * Not yet implemented.
 	 */
-	printf("%s: not supported\n", __FUNCTION__);
+	printf("%s: not supported\n", __func__);
 	return 1;
 }