# HG changeset patch
# User blanchet
# Date 1425553054 -3600
# Node ID 1716da11a11cc5ef865d9c11f8d253c4e0b2a0a5
# Parent  6a7e11fc6ee2a24fd5a2f0bc41b21df217ec90b4
more precise primcorec messages

diff -r 6a7e11fc6ee2 -r 1716da11a11c 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 11:57:34 2015 +0100
@@ -774,7 +774,7 @@
     (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
   let
     val eqn = drop_all eqn0
-      handle TERM _ => error_at ctxt [eqn0] "Ill-formed function equation";
+      handle TERM _ => error_at ctxt [eqn0] "Ill-formed formula";
     val (prems, concl) = Logic.strip_horn eqn
       |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop
         handle TERM _ => error_at ctxt [eqn] "Ill-formed function equation";
@@ -813,8 +813,10 @@
         |>> flat
       else
         error_at ctxt [eqn] "Cannot mix constructor and code views"
+    else if is_some rhs_opt then
+      error_at ctxt [eqn] ("Unexpected equation head: " ^ quote (Syntax.string_of_term ctxt head))
     else
-      error_at ctxt [eqn] "Ill-formed function equation"
+      error_at ctxt [eqn] "Expected equation"
   end;
 
 fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
@@ -1053,15 +1055,10 @@
     val _ = disc_eqnss' |> map (fn x =>
       let val d = duplicates (op = o apply2 #ctr_no) x in
         null d orelse
-        (if forall (is_some o #ctr_rhs_opt) x then
-           error_at lthy
-             (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
-              |> map (the o #ctr_rhs_opt))
-             "Multiple equations for same constructor"
-         else
-           error_at lthy
-             (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)
-             "Extra discriminator formula in definition")
+        error_at lthy
+          (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
+           |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn))
+          "Overspecified constructor cases"
       end);
 
     val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data