src/Pure/Isar/local_theory.ML
changeset 24020 ed4d7abffee7
parent 22846 fb79144af9a3
child 24031 e94e541346d7
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Jul 28 20:40:22 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Jul 28 20:40:24 2007 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  *)
     1.5  
     1.6  type local_theory = Proof.context;
     1.7 +type declaration = morphism -> Context.generic -> Context.generic;
     1.8  
     1.9  signature LOCAL_THEORY =
    1.10  sig
    1.11 @@ -31,9 +32,9 @@
    1.12      local_theory -> (term * (bstring * thm)) list * local_theory
    1.13    val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.14      local_theory -> (bstring * thm list) list * local_theory
    1.15 -  val type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
    1.16 -  val term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
    1.17 -  val declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
    1.18 +  val type_syntax: declaration -> local_theory -> local_theory
    1.19 +  val term_syntax: declaration -> local_theory -> local_theory
    1.20 +  val declaration: declaration -> local_theory -> local_theory
    1.21    val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
    1.22      local_theory -> (term * (bstring * thm)) * local_theory
    1.23    val note: string -> (bstring * Attrib.src list) * thm list ->
    1.24 @@ -67,9 +68,9 @@
    1.25    notes: string ->
    1.26      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.27      local_theory -> (bstring * thm list) list * local_theory,
    1.28 -  type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
    1.29 -  term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
    1.30 -  declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
    1.31 +  type_syntax: declaration -> local_theory -> local_theory,
    1.32 +  term_syntax: declaration -> local_theory -> local_theory,
    1.33 +  declaration: declaration -> local_theory -> local_theory,
    1.34    target_morphism: local_theory -> morphism,
    1.35    target_naming: local_theory -> NameSpace.naming,
    1.36    reinit: local_theory -> theory -> local_theory,