src/HOL/Tools/BNF/bnf_lfp_compat.ML

 Compatibility layer with the old datatype package.
 *)
 
 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 =
 struct
 

 val compatN = "compat_";
 
 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;
 
     fun not_datatype s = error (quote s ^ " is not a new-style datatype");
     fun not_mutually_recursive ss =

     |> Local_Theory.raw_theory register_interpret
     |> Local_Theory.notes all_notes |> snd
   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;