export generic term_syntax;
authorwenzelm
Wed May 17 22:34:50 2006 +0200 (2006-05-17)
changeset 196806a34b1b1f540
parent 19679 ae4c1e2742c1
child 19681 871167b2c70e
export generic term_syntax;
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed May 17 22:34:49 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed May 17 22:34:50 2006 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    val restore_naming: local_theory -> local_theory
     1.5    val naming: local_theory -> local_theory
     1.6    val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
     1.7 +  val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
     1.8    val syntax: string * bool -> (string * mixfix) list -> local_theory -> local_theory
     1.9    val abbrevs: string * bool -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
    1.10    val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
    1.11 @@ -167,18 +168,18 @@
    1.12  
    1.13  (* term syntax *)
    1.14  
    1.15 -fun term_syntax add_thy add_ctxt prmode args ctxt = ctxt |>
    1.16 +fun term_syntax f ctxt = ctxt |>
    1.17    (case locale_of ctxt of
    1.18 -    NONE => theory (add_thy prmode args)
    1.19 +    NONE => theory (Context.theory_map f)
    1.20    | SOME (loc, _) =>
    1.21 -      locale (Locale.add_term_syntax loc (add_ctxt prmode args)) #>
    1.22 -      add_ctxt prmode args);
    1.23 +      locale (Locale.add_term_syntax loc (Context.proof_map f)) #>
    1.24 +      Context.proof_map f);
    1.25  
    1.26 -val syntax = term_syntax Sign.add_const_syntax ProofContext.add_const_syntax;
    1.27 +fun syntax x y =
    1.28 +  term_syntax (Context.mapping (Sign.add_const_syntax x y) (ProofContext.add_const_syntax x y));
    1.29  
    1.30 -fun abbrevs prmode args =
    1.31 -  term_syntax Sign.add_abbrevs ProofContext.add_abbrevs
    1.32 -    prmode (map (fn ((x, mx), rhs) => (x, rhs, mx)) args);
    1.33 +fun abbrevs x y =
    1.34 +  term_syntax (Context.mapping (Sign.add_abbrevs x y) (ProofContext.add_abbrevs x y));
    1.35  
    1.36  
    1.37  (* consts *)