# HG changeset patch
# User wenzelm
# Date 1147481500 -7200
# Node ID c107e7a795598583cf0a62fe6f9ee88a077bbc71
# Parent  de019ddcd89eb1d4d616b2483111cd235a24b37f
added add_defs_unchecked(_i);

diff -r de019ddcd89e -r c107e7a79559 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat May 13 02:51:37 2006 +0200
+++ b/src/Pure/pure_thy.ML	Sat May 13 02:51:40 2006 +0200
@@ -84,6 +84,10 @@
     theory -> thm list * theory
   val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
     theory -> thm list * theory
+  val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list ->
+    theory -> thm list * theory
+  val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
+    theory -> thm list * theory
   val add_defss: bool -> ((bstring * string list) * attribute list) list ->
     theory -> thm list list * theory
   val add_defss_i: bool -> ((bstring * term list) * attribute list) list ->
@@ -466,14 +470,16 @@
   fun add_singles add = fold_map (add_single add);
   fun add_multis add = fold_map (add_multi add);
 in
-  val add_axioms    = add_singles Theory.add_axioms;
-  val add_axioms_i  = add_singles Theory.add_axioms_i;
-  val add_axiomss   = add_multis Theory.add_axioms;
-  val add_axiomss_i = add_multis Theory.add_axioms_i;
-  val add_defs      = add_singles o Theory.add_defs;
-  val add_defs_i    = add_singles o Theory.add_defs_i;
-  val add_defss     = add_multis o Theory.add_defs;
-  val add_defss_i   = add_multis o Theory.add_defs_i;
+  val add_axioms           = add_singles Theory.add_axioms;
+  val add_axioms_i         = add_singles Theory.add_axioms_i;
+  val add_axiomss          = add_multis Theory.add_axioms;
+  val add_axiomss_i        = add_multis Theory.add_axioms_i;
+  val add_defs             = add_singles o (Theory.add_defs false);
+  val add_defs_i           = add_singles o (Theory.add_defs_i false);
+  val add_defs_unchecked   = add_singles o (Theory.add_defs true);
+  val add_defs_unchecked_i = add_singles o (Theory.add_defs_i true);
+  val add_defss            = add_multis o (Theory.add_defs false);
+  val add_defss_i          = add_multis o (Theory.add_defs_i false);
 end;