changeset 52207 | 21026c312cc3 |
parent 52090 | ff1ec795604b |
child 52298 | 608afd26a476 |
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 28 20:00:29 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 28 21:17:48 2013 +0200 @@ -3122,6 +3122,6 @@ val _ = Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes" - (parse_co_datatype_cmd false construct_gfp); + (parse_co_datatype_cmd Greatest_FP construct_gfp); end;