--- a/src/Pure/Thy/thy_parse.ML Tue Nov 17 14:06:32 1998 +0100
+++ b/src/Pure/Thy/thy_parse.ML Tue Nov 17 14:07:04 1998 +0100
@@ -571,7 +571,7 @@
section "path" "|> Theory.add_path" name,
section "global" "|> PureThy.global_path" empty_decl,
section "local" "|> PureThy.local_path" empty_decl,
- section "setup" "|> Theory.apply" long_id,
+ section "setup" "|> Library.apply" long_id,
section "MLtext" "" verbatim,
section "locale" "|> Locale.add_locale" locale_decl];
--- a/src/Pure/pure.ML Tue Nov 17 14:06:32 1998 +0100
+++ b/src/Pure/pure.ML Tue Nov 17 14:07:04 1998 +0100
@@ -18,7 +18,7 @@
val thy =
PureThy.begin_theory "Pure" [ProtoPure.thy]
|> Theory.add_syntax Syntax.pure_appl_syntax
- |> Theory.apply common_setup
+ |> Library.apply common_setup
|> PureThy.end_theory;
end;
@@ -27,7 +27,7 @@
val thy =
PureThy.begin_theory "CPure" [ProtoPure.thy]
|> Theory.add_syntax Syntax.pure_applC_syntax
- |> Theory.apply common_setup
+ |> Library.apply common_setup
|> Theory.copy
|> PureThy.end_theory;
end;
--- 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 **)