# HG changeset patch
# User blanchet
# Date 1457633706 -3600
# Node ID 8c7301325f9f26efaadf5c1ca002166ccfee0105
# Parent  969480bdef55d5a2684514b3ab23a9edce3fe198
don't throw an exception when trying to print an error message

diff -r 969480bdef55 -r 8c7301325f9f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- 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}) ^ ")");