--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 10 18:32:12 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 10 19:15:06 2016 +0100
@@ -131,9 +131,7 @@
error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
fun unsupported_case_around_corec_call ctxt eqns t =
error_at ctxt eqns ("Unsupported corecursive call under case expression " ^
- quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^
- quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^
- " with discriminators and selectors to circumvent this limitation.)");
+ quote (Syntax.string_of_term ctxt t) ^ " for datatype with no discriminators and selectors");
fun use_primcorecursive () =
error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
quote (#1 @{command_keyword primcorec}) ^ ")");