diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Nominal2.thy	Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
   Nominal2_Base Nominal2_Abs Nominal2_FCB
 keywords
   "nominal_datatype" :: thy_decl and
-  "nominal_primrec" "nominal_inductive" :: thy_goal and
+  "nominal_function" "nominal_inductive" :: thy_goal and
   "avoids" "binds"
 begin