Theory.apply replaced by Library.apply;
authorwenzelm
Tue, 17 Nov 1998 14:07:04 +0100
changeset 5905 68cdba6c178f
parent 5904 e077a0e66563
child 5906 1f58694fc3e2
Theory.apply replaced by Library.apply;
src/Pure/Thy/thy_parse.ML
src/Pure/pure.ML
src/Pure/theory.ML
--- 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 **)