src/HOL/BNF/Tools/bnf_gfp.ML
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;