# HG changeset patch
# User wenzelm
# Date 1147481509 -7200
# Node ID 50515882049e8016d6310ce1a59f08e60f95c03e
# Parent  f7aa7d1743430e92fa011f6f48cf9fd22b65e726
added add_primrec_unchecked_i;

diff -r f7aa7d174343 -r 50515882049e src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sat May 13 02:51:48 2006 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Sat May 13 02:51:49 2006 +0200
@@ -12,6 +12,8 @@
     -> 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 =
@@ -221,7 +223,7 @@
     |> 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;
@@ -247,7 +249,9 @@
     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';
@@ -265,6 +269,8 @@
     (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