Theory.apply replaced by Library.apply;
authorwenzelm
Tue Nov 17 14:07:04 1998 +0100 (1998-11-17)
changeset 590568cdba6c178f
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
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Nov 17 14:06:32 1998 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Nov 17 14:07:04 1998 +0100
     1.3 @@ -571,7 +571,7 @@
     1.4    section "path" "|> Theory.add_path" name,
     1.5    section "global" "|> PureThy.global_path" empty_decl,
     1.6    section "local" "|> PureThy.local_path" empty_decl,
     1.7 -  section "setup" "|> Theory.apply" long_id,
     1.8 +  section "setup" "|> Library.apply" long_id,
     1.9    section "MLtext" "" verbatim,
    1.10    section "locale" "|> Locale.add_locale" locale_decl];
    1.11  
     2.1 --- a/src/Pure/pure.ML	Tue Nov 17 14:06:32 1998 +0100
     2.2 +++ b/src/Pure/pure.ML	Tue Nov 17 14:07:04 1998 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4      val thy =
     2.5        PureThy.begin_theory "Pure" [ProtoPure.thy]
     2.6        |> Theory.add_syntax Syntax.pure_appl_syntax
     2.7 -      |> Theory.apply common_setup
     2.8 +      |> Library.apply common_setup
     2.9        |> PureThy.end_theory;
    2.10    end;
    2.11  
    2.12 @@ -27,7 +27,7 @@
    2.13      val thy =
    2.14        PureThy.begin_theory "CPure" [ProtoPure.thy]
    2.15        |> Theory.add_syntax Syntax.pure_applC_syntax
    2.16 -      |> Theory.apply common_setup
    2.17 +      |> Library.apply common_setup
    2.18        |> Theory.copy
    2.19        |> PureThy.end_theory;
    2.20    end;
     3.1 --- a/src/Pure/theory.ML	Tue Nov 17 14:06:32 1998 +0100
     3.2 +++ b/src/Pure/theory.ML	Tue Nov 17 14:07:04 1998 +0100
     3.3 @@ -33,7 +33,6 @@
     3.4  signature THEORY =
     3.5  sig
     3.6    include BASIC_THEORY
     3.7 -  val apply: (theory -> theory) list -> theory -> theory
     3.8    val axiomK: string
     3.9    val oracleK: string
    3.10    (*theory extension primitives*)
    3.11 @@ -136,10 +135,6 @@
    3.12  (*partial Pure theory*)
    3.13  val pre_pure = make_theory Sign.pre_pure Symtab.empty Symtab.empty [] [];
    3.14  
    3.15 -(*apply transformers*)
    3.16 -fun apply [] thy = thy
    3.17 -  | apply (f :: fs) thy = apply fs (f thy);
    3.18 -
    3.19  
    3.20  
    3.21  (** extend theory **)