# HG changeset patch
# User blanchet
# Date 1382784861 -7200
# Node ID 5151b84d06680b40de8817aeb9a340645fa543b5
# Parent  4d3a481fc48e8dcb270c80adabf45bfa962fda7f
tuned error message

diff -r 4d3a481fc48e -r 5151b84d0668 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 25 16:20:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 26 12:54:21 2013 +0200
@@ -495,7 +495,7 @@
     val applied_fun = concl
       |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
       |> the
-      handle Option.Option => primrec_error_eqn "malformed discriminator equation" concl;
+      handle Option.Option => primrec_error_eqn "malformed discriminator formula" concl;
     val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
     val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
 
@@ -868,7 +868,7 @@
       |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
     val _ = disc_eqnss' |> map (fn x =>
       let val d = duplicates ((op =) o pairself #ctr_no) x in null d orelse
-        primrec_error_eqns "excess discriminator equations in definition"
+        primrec_error_eqns "excess discriminator formula in definition"
           (maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) end);
 
     val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data