--- 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