# HG changeset patch
# User blanchet
# Date 1425555131 -3600
# Node ID a93592aedce42783d2014397cebf788e1bf90dba
# Parent  28f53c1b35689d0df7e225b664969e3166066f1c
message tuning

diff -r 28f53c1b3568 -r a93592aedce4 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 12:19:05 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 12:32:11 2015 +0100
@@ -604,13 +604,13 @@
     val _ = null dups orelse error_at ctxt [eqn]
         ("Duplicate variable " ^ quote (Syntax.string_of_term ctxt (hd dups)));
 
+    val _ = forall is_Free fun_args orelse
+      error_at ctxt [eqn] ("Non-variable function argument on left-hand side " ^
+        quote (Syntax.string_of_term ctxt (the (find_first (not o is_Free) fun_args))));
+
     val fixeds = filter (Variable.is_fixed ctxt o fst o dest_Free) fun_args;
     val _ = null fixeds orelse error_at ctxt [eqn] ("Function argument " ^
         quote (Syntax.string_of_term ctxt (hd fixeds)) ^ " is fixed in context");
-
-    val _ = forall is_Free fun_args orelse
-      error_at ctxt [eqn] ("Non-variable function argument \"" ^
-        Syntax.string_of_term ctxt (the (find_first (not o is_Free) fun_args)));
   in () end;
 
 fun dissect_coeqn_disc ctxt fun_names sequentials
@@ -789,7 +789,7 @@
       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";
+        handle TERM _ => error_at ctxt [eqn] "Ill-formed equation";
 
     val head = concl
       |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
@@ -834,9 +834,9 @@
       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))
+      error_at ctxt [eqn] ("Ill-formed equation head: " ^ quote (Syntax.string_of_term ctxt head))
     else
-      error_at ctxt [eqn] "Expected equation"
+      error_at ctxt [eqn] "Expected equation or discriminator formula"
   end;
 
 fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
@@ -1511,6 +1511,9 @@
 
 fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
   let
+    val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
+    val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
+
     val (raw_specs, of_specs_opt) =
       split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
     val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);