removed add_thms_as_axms;
authorwenzelm
Fri, 24 Oct 1997 17:11:48 +0200
changeset 3988 6ff1a1e2bd21
parent 3987 22f5291012df
child 3989 092ab30c1471
removed add_thms_as_axms;
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