1.1 --- a/src/Pure/pure_thy.ML	Tue Oct 02 22:23:28 2007 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Oct 02 22:23:30 2007 +0200
     1.3 @@ -94,10 +94,6 @@
     1.4      theory -> thm list * theory
     1.5    val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
     1.6      theory -> thm list * theory
     1.7 -  val add_defss: bool -> ((bstring * string list) * attribute list) list ->
     1.8 -    theory -> thm list list * theory
     1.9 -  val add_defss_i: bool -> ((bstring * term list) * attribute list) list ->
    1.10 -    theory -> thm list list * theory
    1.11    val appl_syntax: (string * typ * mixfix) list
    1.12    val applC_syntax: (string * typ * mixfix) list
    1.13  end;
    1.14 @@ -489,8 +485,6 @@
    1.15    val add_defs_i           = add_singles o Theory.add_defs_i false;
    1.16    val add_defs_unchecked   = add_singles o Theory.add_defs true;
    1.17    val add_defs_unchecked_i = add_singles o Theory.add_defs_i true;
    1.18 -  val add_defss            = add_multis o Theory.add_defs false;
    1.19 -  val add_defss_i          = add_multis o Theory.add_defs_i false;
    1.20  end;
    1.21  
    1.22