src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML

   let val thy = Proof_Context.theory_of lthy in
     Raw_Simplifier.rewrite_term thy unfold_id_thms1 []
     #> Raw_Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} []
   end;
 
-fun unexpected_corec_call ctxt eqns t =
-  error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
-fun unsupported_case_around_corec_call ctxt eqns t =
-  error_at ctxt eqns ("Unsupported corecursive call under case expression " ^
-    quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^
-    quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^
-    " with  discriminators and selectors to circumvent this limitation.)");
-
 datatype corec_option =
   Plugins_Option of Proof.context -> Plugin_Name.filter |
   Friend_Option |
   Transfer_Option;
 

   let
     val (fun_t, arg_ts) = strip_comb lhs;
 
     fun check_fun_name () =
       null fun_frees orelse member (op aconv) fun_frees fun_t orelse
-      error (quote (Syntax.string_of_term ctxt fun_t) ^
-        " is not the function currently being defined");
-
-    fun check_args_are_vars () =
-      let
-        fun is_ok_Free_or_Var (Free (s, _)) = not (String.isSuffix inner_fp_suffix s)
-          | is_ok_Free_or_Var (Var _) = true
-          | is_ok_Free_or_Var _ = false;
-
-        fun is_valid arg =
-          (is_ok_Free_or_Var arg andalso not (member (op aconv) fun_frees arg)) orelse
-          error ("Argument " ^ quote (Syntax.string_of_term ctxt arg) ^ " is not free");
-      in
-        forall is_valid arg_ts
-      end;
-
-    fun check_no_duplicate_arg () =
-      (case duplicates (op =) arg_ts of
-        [] => ()
-      | arg :: _ => error ("Repeated argument: " ^ quote (Syntax.string_of_term ctxt arg)));
+      ill_formed_equation_head ctxt [] fun_t;
 
     fun check_no_other_frees () =
       (case Term.add_frees rhs [] |> map Free |> subtract (op =) (fun_frees @ arg_ts)
-          |> filter_out (Variable.is_fixed ctxt o fst o dest_Free) of
-        [] => ()
-      | Free (s, _) :: _ => error ("Extra variable on right-hand side: " ^ quote s));
-  in
-    check_no_duplicate_arg ();
+          |> find_first (not o Variable.is_fixed ctxt o fst o dest_Free) of
+        NONE => ()
+      | SOME t => extra_variable_in_rhs ctxt [] t);
+  in
+    check_duplicate_variables_in_lhs ctxt [] arg_ts;
     check_fun_name ();
-    check_args_are_vars ();
+    check_all_fun_arg_frees ctxt [] (filter_out is_Var arg_ts);
     check_no_other_frees ()
   end;
 
 fun parse_corec_equation ctxt fun_frees eq =
   let
     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (drop_all eq))
-      handle TERM _ => error "Expected HOL equation";
+      handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eq];
 
     val _ = check_corec_equation ctxt fun_frees (lhs, rhs);
 
     val (fun_t, arg_ts) = strip_comb lhs;
     val (arg_Ts, _) = strip_type (fastype_of fun_t);

               explore params t
           end
         | NONE => explore params t)
       | _ => explore params t)
     and explore_cond params t =
-      if has_self_call t then
-        error ("Unallowed corecursive call in condition " ^ quote (Syntax.string_of_term lthy t))
-      else
-        explore_inner params t
+      if has_self_call t then unexpected_rec_call_in lthy [] t else explore_inner params t
     and explore_inner params t =
       massage_rho explore_inner_general params t
     and explore_inner_general (params as {bound_Us, bound_Ts, T, ...}) t =
       let val (fun_t, arg_ts) = strip_comb t in
         if is_constant t then

                 fun_t $ arg'
               else if arg_U = YpreT then
                 disc' $ arg'
               else
                 error ("Discriminator " ^ quote (Syntax.string_of_term lthy fun_t) ^
-                  " cannot be applied to non-lhs argument " ^
+                  " cannot be applied to non-variable " ^
                   quote (Syntax.string_of_term lthy (hd arg_ts)))
             end
           | _ =>
             (case as_member_of sels fun_t of
               SOME sel' =>

                   build_function_after_encapsulation fun_t fun_t params arg_ts arg_ts'
                 else if arg_U = YpreT then
                   build_function_after_encapsulation fun_t sel' params arg_ts arg_ts'
                 else
                   error ("Selector " ^ quote (Syntax.string_of_term lthy fun_t) ^
-                    " cannot be applied to non-lhs argument " ^
+                    " cannot be applied to non-variable " ^
                     quote (Syntax.string_of_term lthy (hd arg_ts)))
               end
             | NONE =>
               (case as_member_of friends fun_t of
                 SOME (_, friend') =>

         val ctr_opt = as_member_of ctr_guards fun_t;
       in
         if is_some ctr_opt then
           rebuild_function_after_exploration fun_t (the ctr_opt) explore_inner params arg_ts
         else
-          error ("Constructor expected on right-hand side, " ^
-            quote (Syntax.string_of_term lthy fun_t) ^ " found instead")
+          not_constructor_in_rhs lthy [] fun_t
       end;
 
     val rho_rhs = rhs
       |> explore_ctr (build_params [] [] (fastype_of rhs))
       |> abs_tuple_balanced (map (map_types (fpT_to YpreT)) lhs_args)

     val rho_rhsZ = substT Y Z rho_rhs;
   in
     HOLogic.mk_Trueprop (rho_rel $ rho_rhs $ rho_rhsZ)
   end;
 
-fun extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT fun_T k_T
-    ssig_T ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy =
-  let
-    val Type (fpT_name, _) = body_type fun_T;
-
+fun extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
+    ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy =
+  let
     fun mk_rel T bnf =
       let
         val ZT = Tsubst Y Z T;
         val rel_T = mk_predT [mk_pred2T Y Z, T, ZT];
       in

       else
         explore params t
 
     fun massage_let_if_case_corec explore {bound_Ts, U, T, ...} t =
       massage_let_if_case ctxt has_self_call (fn bound_Ts => explore (build_params bound_Ts U T))
-        (K (unexpected_corec_call ctxt [t])) (K (unsupported_case_around_corec_call ctxt [t]))
+        (K (unexpected_corec_call_in ctxt [t])) (K (unsupported_case_around_corec_call ctxt [t]))
         bound_Ts t;
 
     val massage_map_let_if_case =
       massage_star [massage_map_corec, massage_fun, massage_comp, massage_let_if_case_corec];
 

 
     val (plugins, friend, transfer) = get_options lthy opts;
     val ([((b, fun_T), mx)], [(_, eq)]) =
       fst (Specification.read_multi_specs raw_fixes [((Binding.empty_atts, raw_eq), [], [])] lthy);
 
-    val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
-      error ("Type of " ^ Binding.print b ^ " contains top sort");
+    val _ = check_top_sort lthy b fun_T;
 
     val (arg_Ts, res_T) = strip_type fun_T;
     val fpT_name = (case res_T of Type (s, _) => s | _ => not_codatatype lthy res_T);
     val fun_free = Free (Binding.name_of b, fun_T);
     val parsed_eq = parse_corec_equation lthy [fun_free] eq;

         val friend_parse_info = friend_parse_info_of lthy arg_Ts res_T buffer;
 
         val parsed_eq' = parsed_eq ||> subst_atomic [(fun_free, fun_t)];
       in
         lthy
-        |> extract_rho_return_transfer_goals b version dead_pre_bnf dead_k_bnf Y Z preT fun_T k_T
-          ssig_T ssig_fp_sugar friend_parse_info fun_t parsed_eq'
+        |> extract_rho_return_transfer_goals b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
+          ssig_fp_sugar friend_parse_info fun_t parsed_eq'
         |>> pair prepared
       end;
 
     val ((prepareds, (rho_datas, transfer_goal_datas)), lthy) =
       if friend then extract_rho lthy |>> (apfst single ##> (apfst single #> apsnd single))

     val code_goal = Syntax.read_prop fake_lthy raw_eq;
 
     val fun_T =
       (case code_goal of
         @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _) => fastype_of (head_of t)
-      | _ => error "Expected HOL equation");
+      | _ => ill_formed_equation_lhs_rhs lthy [code_goal]);
     val fun_t = Const (fun_name, fun_T);
 
     val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T;
 
     val no_base = has_no_corec_info lthy fpT_name;

     val friend_parse_info = friend_parse_info_of lthy arg_Ts res_T buffer;
 
     val parsed_eq = parse_corec_equation lthy [] code_goal;
 
     val (((rho, rho_def), (const_transfer_goals, rho_transfer_goal)), lthy) =
-      extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT fun_T k_T
-        ssig_T ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy;
+      extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
+        ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy;
 
     fun register_friend_extra_and_note_thms code_goal code_thm const_transfers k_T friend_info
         lthy =
       let
         val (corec_info, lthy) = corec_info_of res_T lthy;