# HG changeset patch
# User blanchet
# Date 1425553054 -3600
# Node ID bd66d9b93a6b3b5c5fa4bc188f5c0628410ca390
# Parent  b44f128d24f257ee5019fc941671a51178cb90ce
improved primcorec messages

diff -r b44f128d24f2 -r bd66d9b93a6b 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
@@ -657,7 +657,15 @@
     val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
     val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
 
-    val catch_all = (try (fst o dest_Free o the_single) prems0 = SOME Name.uu_);
+    fun is_catch_all_prem (Free (s, _)) = s = Name.uu_
+      | is_catch_all_prem _ = false;
+
+    val catch_all =
+      (case prems0 of
+        [prem] => is_catch_all_prem prem
+      | _ =>
+        if exists is_catch_all_prem prems0 then error_at ctxt [concl] "Superfluous premises"
+        else false);
     val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
     val prems = map (abstract (List.rev fun_args)) prems0;
     val actual_prems =
@@ -788,8 +796,10 @@
       |> head_of;
 
     val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd);
-    val _ = is_none rhs_opt orelse not (can dest_funT (fastype_of (the rhs_opt))) orelse
-      error_at ctxt [eqn] "Expected more arguments to function on left-hand side";
+
+    fun check_num_args () =
+      is_none rhs_opt orelse not (can dest_funT (fastype_of (the rhs_opt))) orelse
+        error_at ctxt [eqn] "Expected more arguments to function on left-hand side";
 
     val discs = maps (map #disc) basic_ctr_specss;
     val sels = maps (maps #sels) basic_ctr_specss;
@@ -799,24 +809,28 @@
        (is_some rhs_opt andalso
         member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso
         member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then
-      dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
-        matchedsss
-      |>> single
+      (check_num_args ();
+       dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
+         matchedsss
+       |>> single)
     else if member (op =) sels head then
       (null prems orelse error_at ctxt [eqn] "Unexpected condition in selector formula";
+       check_num_args ();
        ([dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt
            concl], matchedsss))
     else if is_some rhs_opt andalso is_Free head andalso is_free_in fun_names head then
       if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then
-        dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0
-          (if null prems then
-             SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
-           else
-             NONE)
-          prems concl matchedsss
+        (check_num_args ();
+         dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0
+           (if null prems then
+              SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
+            else
+              NONE)
+           prems concl matchedsss)
       else if null prems then
-        dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
-        |>> flat
+        (check_num_args ();
+         dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
+         |>> flat)
       else
         error_at ctxt [eqn] "Cannot mix constructor and code views"
     else if is_some rhs_opt then