--- 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;