# HG changeset patch
# User wenzelm
# Date 1147481502 -7200
# Node ID d370c3f5d3b22954ad3e2d19b6dd245f7e57bd44
# Parent  c107e7a795598583cf0a62fe6f9ee88a077bbc71
Theory.add_defs(_i): added unchecked flag;

diff -r c107e7a79559 -r d370c3f5d3b2 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat May 13 02:51:40 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sat May 13 02:51:42 2006 +0200
@@ -170,7 +170,7 @@
 		val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
 		           (*Theory is augmented with the constant, then its def*)
 		val cdef = cname ^ "_def"
-		val thy'' = Theory.add_defs_i false [(cdef, def)] thy'
+		val thy'' = Theory.add_defs_i false false [(cdef, def)] thy'
 	    in dec_sko (subst_bound (list_comb(c,args), p)) 
 	               (n+1, (thy'', get_axiom thy'' cdef :: axs)) 
 	    end
diff -r c107e7a79559 -r d370c3f5d3b2 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat May 13 02:51:40 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat May 13 02:51:42 2006 +0200
@@ -248,7 +248,7 @@
 local
 
 fun add_def (name, prop) =
-  Theory.add_defs_i false [(name, prop)] #> (fn thy =>
+  Theory.add_defs_i false false [(name, prop)] #> (fn thy =>
     let
       val th = Thm.get_axiom_i thy (Sign.full_name thy name);
       val cert = Thm.cterm_of thy;
diff -r c107e7a79559 -r d370c3f5d3b2 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat May 13 02:51:40 2006 +0200
+++ b/src/Pure/theory.ML	Sat May 13 02:51:42 2006 +0200
@@ -49,8 +49,8 @@
   val assert_super: theory -> theory -> theory
   val add_axioms: (bstring * string) list -> theory -> theory
   val add_axioms_i: (bstring * term) list -> theory -> theory
-  val add_defs: bool -> (bstring * string) list -> theory -> theory
-  val add_defs_i: bool -> (bstring * term) list -> theory -> theory
+  val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
+  val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
@@ -254,7 +254,7 @@
 
 (* check_def *)
 
-fun check_def thy overloaded (bname, tm) defs =
+fun check_def thy unchecked overloaded (bname, tm) defs =
   let
     val pp = Sign.pp thy;
     fun prt_const (c, T) =
@@ -266,7 +266,7 @@
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in
-    defs |> Defs.define (Sign.const_typargs thy) true (Context.theory_name thy)
+    defs |> Defs.define (Sign.const_typargs thy) unchecked true (Context.theory_name thy)
       name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
   end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
@@ -278,10 +278,10 @@
 
 local
 
-fun gen_add_defs prep_axm overloaded raw_axms thy =
+fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
   let val axms = map (prep_axm thy) raw_axms in
     thy
-    |> map_defs (fold (check_def thy overloaded) axms)
+    |> map_defs (fold (check_def thy unchecked overloaded) axms)
     |> add_axioms_i axms
   end;
 
@@ -302,7 +302,7 @@
     fun const_of (Const const) = const
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
-    fun specify (c, T) = Defs.define (Sign.const_typargs thy) false (Context.theory_name thy)
+    fun specify (c, T) = Defs.define (Sign.const_typargs thy) false false (Context.theory_name thy)
       (c ^ " axiom") (prep_const thy (c, T)) [];
     val finalize = specify o check_overloading thy overloaded o
       const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;