src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

 val selN = "sel";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
 
+fun extra_variable ctxt ts var =
+  error_at ctxt ts ("Extra variable " ^ quote (Syntax.string_of_term ctxt var));
 fun not_codatatype ctxt T =
   error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
 fun ill_formed_corec_call ctxt t =
   error ("Ill-formed corecursive call " ^ quote (Syntax.string_of_term ctxt t));
 fun invalid_map ctxt t =

   Sel of coeqn_data_sel;
 
 fun is_free_in frees (Free (v, _)) = member (op =) frees v
   | is_free_in _ _ = false;
 
-fun check_extra_variables ctxt vars names eqn =
-  let val b = fold_aterms (fn x as Free (v, _) =>
-    if (not (member (op =) vars x) andalso
-      not (member (op =) names v) andalso
-      v <> Name.uu_ andalso
-      not (Variable.is_fixed ctxt v)) then cons x else I | _ => I) eqn []
-  in
-    null b orelse error_at ctxt [eqn]
-      ("Extra variable " ^ quote (Syntax.string_of_term ctxt (hd b)))
+fun add_extra_frees ctxt frees names =
+  fold_aterms (fn x as Free (v, _) =>
+    (not (member (op =) frees x) andalso not (member (op =) names v) andalso
+     not (Variable.is_fixed ctxt v) andalso v <> Name.uu_)
+    ? cons x | _ => I);
+
+fun check_extra_frees ctxt frees names t =
+  let val bads = add_extra_frees ctxt frees names t [] in
+    null bads orelse extra_variable ctxt [t] (hd bads)
   end;
 
 fun dissect_coeqn_disc ctxt fun_names sequentials
     (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos ctr_rhs_opt code_rhs_opt prems0
     concl matchedsss =

     val user_eqn =
       (actual_prems, concl)
       |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args)
       |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies;
 
-    val _ = check_extra_variables ctxt fun_args fun_names user_eqn;
+    val _ = check_extra_frees ctxt fun_args fun_names user_eqn;
   in
     (Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
        disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt,
        code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn},
      matchedsss')

         SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
       | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
           handle List.Empty => error_at ctxt [eqn] "Ambiguous selector (without \"of\")");
     val user_eqn = drop_all eqn0;
 
-    val _ = check_extra_variables ctxt fun_args fun_names user_eqn;
+    val _ = check_extra_frees ctxt fun_args fun_names user_eqn;
   in
     Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel,
       rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos,
       user_eqn = user_eqn}
   end;

     eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
   let
     val (lhs, rhs) = HOLogic.dest_eq concl;
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
 
-    val _ = check_extra_variables ctxt fun_args fun_names (drop_all eqn0);
+    val _ = check_extra_frees ctxt fun_args fun_names (drop_all eqn0);
 
     val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
     val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
     val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
       handle Option.Option => error_at ctxt [ctr] "Not a constructor";

 fun dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss =
   let
     val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs ctxt has_call []);
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
 
-    val _ = check_extra_variables ctxt fun_args fun_names concl;
+    val _ = check_extra_frees ctxt fun_args fun_names concl;
 
     val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
 
     val cond_ctrs = fold_rev_corec_code_rhs ctxt (fn cs => fn ctr => fn _ =>
         if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs)

           if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False})
           else Const (@{const_name undefined}, T))
       |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
       |> fold2 (fold o build_corec_args_sel ctxt has_call) sel_eqnss ctr_specss;
 
+    val bad = fold (add_extra_frees ctxt [] []) corec_args [];
+    val _ = null bad orelse
+      (if exists has_call corec_args then nonprimitive_corec ctxt []
+       else extra_variable ctxt [] (hd bad));
+
     fun currys [] t = t
       | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
           |> fold_rev (Term.abs o pair Name.uu) Ts;
 
     val excludess' =

               |> 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)
-             "Excess discriminator formula in definition")
+             "Extra discriminator formula in definition")
       end);
 
     val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
       |> partition_eq (op = o apply2 #fun_name)
       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names