add_defs(_i): overloaded option;

--- a/src/Pure/Isar/isar_thy.ML	Thu Jul 13 23:14:15 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 13 23:14:49 2000 +0200
@@ -51,8 +51,9 @@
   val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
   val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
     -> theory -> theory
-  val add_defs: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
-  val add_defs_i: (((bstring * term) * theory attribute list) * Comment.text) list
+  val add_defs: bool * (((bstring * string) * Args.src list) * Comment.text) list
+    -> theory -> theory
+  val add_defs_i: bool * (((bstring * term) * theory attribute list) * Comment.text) list
     -> theory -> theory
   val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list
     -> theory -> theory
@@ -263,8 +264,8 @@
 
 val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
 val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
-val add_defs = add_axms (#1 oo PureThy.add_defs) o map Comment.ignore;
-val add_defs_i = (#1 oo PureThy.add_defs_i) o map Comment.ignore;
+fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) (map Comment.ignore args);
+fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) (map Comment.ignore args);
 
 
 (* constdefs *)
@@ -272,7 +273,7 @@
 fun gen_add_constdefs consts defs args thy =
   thy
   |> consts (map (Comment.ignore o fst) args)
-  |> defs (map (fn (((c, _, mx), _), (s, _)) =>
+  |> defs (false, map (fn (((c, _, mx), _), (s, _)) =>
     (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
 
 fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args;

--- a/src/Pure/pure_thy.ML	Thu Jul 13 23:14:15 2000 +0200
+++ b/src/Pure/pure_thy.ML	Thu Jul 13 23:14:49 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/pure_thy.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theorem database, derived theory operations, and the ProtoPure theory.
 *)
@@ -38,10 +39,14 @@
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
   val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
   val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list
-  val add_defs: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
-  val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
-  val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
-  val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list
+  val add_defs: bool -> ((bstring * string) * theory attribute list) list
+    -> theory -> theory * thm list
+  val add_defs_i: bool -> ((bstring * term) * theory attribute list) list
+    -> theory -> theory * thm list
+  val add_defss: bool -> ((bstring * string list) * theory attribute list) list
+    -> theory -> theory * thm list list
+  val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list
+    -> theory -> theory * thm list list
   val get_name: theory -> string
   val put_name: string -> theory -> theory
   val global_path: theory -> theory
@@ -323,10 +328,10 @@
   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 Theory.add_defs;
-  val add_defs_i    = add_singles Theory.add_defs_i;
-  val add_defss     = add_multis Theory.add_defs;
-  val add_defss_i   = add_multis Theory.add_defs_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;
 end;
 
 
@@ -451,7 +456,7 @@
   |> Theory.add_modesyntax ("", false)
     [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   |> local_path
-  |> (#1 oo (add_defs o map Thm.no_attributes))
+  |> (#1 oo (add_defs false o map Thm.no_attributes))
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
     ("Goal_def", "GOAL (PROP A) == PROP A")]
   |> (#1 o add_thmss [(("nothing", []), [])])