# HG changeset patch
# User wenzelm
# Date 1191356610 -7200
# Node ID 636b23afee76cba5fb352ba9eb5086e8514a7d11
# Parent  2d0fa8f31804f719275dbf6adfdf8806b12f36f9
removed unused add_defss;

diff -r 2d0fa8f31804 -r 636b23afee76 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Oct 02 22:23:28 2007 +0200
+++ b/src/Pure/pure_thy.ML	Tue Oct 02 22:23:30 2007 +0200
@@ -94,10 +94,6 @@
     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 ->
-    theory -> thm list list * theory
   val appl_syntax: (string * typ * mixfix) list
   val applC_syntax: (string * typ * mixfix) list
 end;
@@ -489,8 +485,6 @@
   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;