1.1 --- a/src/Pure/Isar/isar_thy.ML	Sat May 13 02:51:43 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Sat May 13 02:51:45 2006 +0200
     1.3 @@ -8,14 +8,12 @@
     1.4  signature ISAR_THY =
     1.5  sig
     1.6    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
     1.7 -  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> theory
     1.8 -  val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
     1.9 -  val add_defs_i: bool * ((bstring * term) * attribute list) list -> theory -> theory
    1.10 +  val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    1.11    val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    1.12    val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    1.13    val theorems: string ->
    1.14      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.15 -    -> theory -> (string * thm list) list * theory 
    1.16 +    -> theory -> (string * thm list) list * theory
    1.17    val theorems_i: string ->
    1.18      ((bstring * attribute list) * (thm list * attribute list) list) list
    1.19      -> theory -> (string * thm list) list * theory
    1.20 @@ -59,9 +57,10 @@
    1.21    f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
    1.22  
    1.23  val add_axioms = add_axms (snd oo PureThy.add_axioms);
    1.24 -val add_axioms_i = snd oo PureThy.add_axioms_i;
    1.25 -fun add_defs (x, args) = add_axms (snd oo PureThy.add_defs x) args;
    1.26 -fun add_defs_i (x, args) = (snd oo PureThy.add_defs_i x) args;
    1.27 +
    1.28 +fun add_defs ((unchecked, overloaded), args) =
    1.29 +  add_axms
    1.30 +    (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args;
    1.31  
    1.32  
    1.33  (* theorems *)