# HG changeset patch
# User wenzelm
# Date 877705908 -7200
# Node ID 6ff1a1e2bd21672c92dc103a24ce8d7ca02c30e6
# Parent  22f5291012dfef7d63abbbd00b40e5219c7ceea0
removed add_thms_as_axms;

diff -r 22f5291012df -r 6ff1a1e2bd21 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Oct 24 17:11:23 1997 +0200
+++ b/src/Pure/axclass.ML	Fri Oct 24 17:11:48 1997 +0200
@@ -7,7 +7,6 @@
 
 signature AX_CLASS =
 sig
-  val add_thms_as_axms: (string * thm) list -> theory -> theory
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
   val add_axclass: bclass * xclass list -> (string * string) list
@@ -126,10 +125,6 @@
     else prop
   end;
 
-(*general theorems*)
-fun add_thms_as_axms thms thy =
-  Theory.add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
-
 (*theorems expressing class relations*)
 fun add_classrel_thms thms thy =
   let