src/Pure/Isar/local_theory.ML
changeset 24949 5f00e3532418
parent 24933 5471b164813b
child 24984 952045a8dcf2
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Oct 10 17:31:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Oct 10 17:31:56 2007 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    val declaration: declaration -> local_theory -> local_theory
     1.5    val note: string -> (bstring * Attrib.src list) * thm list ->
     1.6      local_theory -> (bstring * thm list) * local_theory
     1.7 -  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.8 +  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.9    val target_morphism: local_theory -> morphism
    1.10    val target_naming: local_theory -> NameSpace.naming
    1.11    val target_name: local_theory -> bstring -> string
    1.12 @@ -167,9 +167,9 @@
    1.13    ProofContext.export_morphism lthy (target_of lthy) $>
    1.14    Morphism.thm_morphism Goal.norm_result;
    1.15  
    1.16 -fun notation mode raw_args lthy =
    1.17 +fun notation add mode raw_args lthy =
    1.18    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    1.19 -  in term_syntax (ProofContext.target_notation mode args) lthy end;
    1.20 +  in term_syntax (ProofContext.target_notation add mode args) lthy end;
    1.21  
    1.22  val target_name = NameSpace.full o target_naming;
    1.23