# HG changeset patch # User wenzelm # Date 911308024 -3600 # Node ID 68cdba6c178fc40e8fc8da65c49a07ad3e38ef33 # Parent e077a0e66563a2374a0b95022fb9d6b199d1d059 Theory.apply replaced by Library.apply; diff -r e077a0e66563 -r 68cdba6c178f src/Pure/Thy/thy_parse.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]; diff -r e077a0e66563 -r 68cdba6c178f src/Pure/pure.ML --- 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; diff -r e077a0e66563 -r 68cdba6c178f src/Pure/theory.ML --- 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 **)