--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 12 15:25:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 12 15:25:17 2013 +0200
@@ -953,12 +953,12 @@
end;
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
- (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
+ (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
- val _ = if fp = Greatest_FP andalso no_dests then
- error "Cannot define destructor-less codatatypes"
+ val _ = if fp = Greatest_FP andalso no_discs_sels then
+ error "Cannot define codatatypes without discriminators and selectors"
else
();