# HG changeset patch
# User blanchet
# Date 1514895392 -3600
# Node ID a2d7c0987f1987fdd042d51320df83abd7491d64
# Parent  0d25e02759b744d1a146deb49c41582cf3038e89
avoid call to function that may throw an exception in error message

diff -r 0d25e02759b7 -r a2d7c0987f19 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Jan 01 23:07:24 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Tue Jan 02 13:16:32 2018 +0100
@@ -172,9 +172,8 @@
   error_at ctxt ats ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
 fun unsupported_case_around_corec_call ctxt ats t =
   error_at ctxt ats ("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) ^
+    "\n(Define datatype with discriminators and selectors to circumvent this limitation)");
 
 fun no_equation_for_ctr_warning ctxt ats ctr =
   warning_at ctxt ats ("No equation for constructor " ^ quote (Syntax.string_of_term ctxt ctr));