--- a/src/Pure/theory.ML Tue Nov 17 14:06:32 1998 +0100
+++ b/src/Pure/theory.ML Tue Nov 17 14:07:04 1998 +0100
@@ -33,7 +33,6 @@
signature THEORY =
sig
include BASIC_THEORY
- val apply: (theory -> theory) list -> theory -> theory
val axiomK: string
val oracleK: string
(*theory extension primitives*)
@@ -136,10 +135,6 @@
(*partial Pure theory*)
val pre_pure = make_theory Sign.pre_pure Symtab.empty Symtab.empty [] [];
-(*apply transformers*)
-fun apply [] thy = thy
- | apply (f :: fs) thy = apply fs (f thy);
-
(** extend theory **)