diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 13:31:42 2014 +0100
@@ -7,7 +7,7 @@
 
 signature BNF_LFP_COMPAT =
 sig
-  val datatype_new_compat_cmd : string list -> local_theory -> local_theory
+  val datatype_compat_cmd : string list -> local_theory -> local_theory
 end;
 
 structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -24,7 +24,7 @@
 val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
 
 (* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
-fun datatype_new_compat_cmd raw_fpT_names lthy =
+fun datatype_compat_cmd raw_fpT_names lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
@@ -203,8 +203,8 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
+  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
     "register new-style datatypes as old-style datatypes"
-    (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
+    (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
 
 end;