# HG changeset patch
# User blanchet
# Date 1425554345 -3600
# Node ID 28f53c1b35689d0df7e225b664969e3166066f1c
# Parent  bd66d9b93a6b3b5c5fa4bc188f5c0628410ca390
tuning

diff -r bd66d9b93a6b -r 28f53c1b3568 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 11:57:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 12:19:05 2015 +0100
@@ -1082,7 +1082,7 @@
         error_at lthy
           (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) dups
            |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn))
-          "Overspecified discriminator case(s)"
+          "Overspecified case(s)"
       end);
 
     val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
@@ -1096,7 +1096,7 @@
         error_at lthy
           (maps (fn t => filter (curry (op =) (ctr_sel_of t) o ctr_sel_of) x) dups
            |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn))
-          "Overspecified selector case(s)"
+          "Overspecified case(s)"
       end);
 
     val arg_Tss = map (binder_types o snd o fst) fixes;