--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 11:30:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Mon Sep 03 11:54:21 2012 +0200
@@ -1755,7 +1755,7 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "bnf_data"} "least fixed points for BNF equations"
+ Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations"
(Parse.and_list1
((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >>
(fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));