changeset 52207 | 21026c312cc3 |
parent 52100 | e58762f34639 |
child 52312 | f461dca57c66 |
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 28 20:00:29 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 28 21:17:48 2013 +0200 @@ -1866,6 +1866,6 @@ val _ = Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" - (parse_co_datatype_cmd true construct_lfp); + (parse_co_datatype_cmd Least_FP construct_lfp); end;