| changeset 71245 | e5664a75f4b5 |
| parent 70494 | 41108e3e9ca5 |
| child 72154 | 2b41b710f6ef |
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Dec 05 21:03:06 2019 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Dec 06 11:12:55 2019 +0100 @@ -1870,6 +1870,4 @@ Outer_Syntax.local_theory \<^command_keyword>\<open>datatype\<close> "define inductive datatypes" (parse_co_datatype_cmd Least_FP construct_lfp); -val _ = Theory.setup (fp_antiquote_setup \<^binding>\<open>datatype\<close>); - end;