src/HOL/Tools/primrec_package.ML

 sig
   val quiet_mode: bool ref
   val add_primrec: string -> ((bstring * string) * Attrib.src list) list
     -> theory -> theory * thm list
   val add_primrec_i: string -> ((bstring * term) * attribute list) list
+    -> theory -> theory * thm list
+  val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
     -> theory -> theory * thm list
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
 struct

     induction
     |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
     |> RuleCases.save induction
   end;
 
-fun add_primrec_i alt_name eqns_atts thy =
+fun gen_primrec unchecked alt_name eqns_atts thy =
   let
     val (eqns, atts) = split_list eqns_atts;
     val sg = Theory.sign_of thy;
     val dt_info = DatatypePackage.get_datatypes thy;
     val rec_eqns = foldr (process_eqn sg) [] (map snd eqns);

     val nameTs1 = map snd fnameTs;
     val nameTs2 = map fst rec_eqns;
     val primrec_name =
       if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
     val (defs_thms', thy') = thy |> Theory.add_path primrec_name |>
-      (if eq_set (nameTs1, nameTs2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
+      (if eq_set (nameTs1, nameTs2) then
+         ((if unchecked then PureThy.add_defs_unchecked_i else PureThy.add_defs_i) false o
+           map Thm.no_attributes) defs'
        else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
          "\nare not mutually recursive"));
     val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
     val _ = message ("Proving equations for primrec function(s) " ^
       commas_quote (map fst nameTs1) ^ " ...");

       |> Theory.parent_path
   in
     (thy''', simps')
   end;
 
+val add_primrec_i = gen_primrec false;
+val add_primrec_unchecked_i = gen_primrec true;
 
 fun add_primrec alt_name eqns thy =
   let
     val sign = Theory.sign_of thy;
     val ((names, strings), srcss) = apfst split_list (split_list eqns);