# HG changeset patch
# User wenzelm
# Date 1147898090 -7200
# Node ID 6a34b1b1f540a1e92b226daf8c24c2f9a0239ede
# Parent  ae4c1e2742c1fa812de5dc0bbcfafb00455b976f
export generic term_syntax;

diff -r ae4c1e2742c1 -r 6a34b1b1f540 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed May 17 22:34:49 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed May 17 22:34:50 2006 +0200
@@ -24,6 +24,7 @@
   val restore_naming: local_theory -> local_theory
   val naming: local_theory -> local_theory
   val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
+  val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
   val syntax: string * bool -> (string * mixfix) list -> local_theory -> local_theory
   val abbrevs: string * bool -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
   val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
@@ -167,18 +168,18 @@
 
 (* term syntax *)
 
-fun term_syntax add_thy add_ctxt prmode args ctxt = ctxt |>
+fun term_syntax f ctxt = ctxt |>
   (case locale_of ctxt of
-    NONE => theory (add_thy prmode args)
+    NONE => theory (Context.theory_map f)
   | SOME (loc, _) =>
-      locale (Locale.add_term_syntax loc (add_ctxt prmode args)) #>
-      add_ctxt prmode args);
+      locale (Locale.add_term_syntax loc (Context.proof_map f)) #>
+      Context.proof_map f);
 
-val syntax = term_syntax Sign.add_const_syntax ProofContext.add_const_syntax;
+fun syntax x y =
+  term_syntax (Context.mapping (Sign.add_const_syntax x y) (ProofContext.add_const_syntax x y));
 
-fun abbrevs prmode args =
-  term_syntax Sign.add_abbrevs ProofContext.add_abbrevs
-    prmode (map (fn ((x, mx), rhs) => (x, rhs, mx)) args);
+fun abbrevs x y =
+  term_syntax (Context.mapping (Sign.add_abbrevs x y) (ProofContext.add_abbrevs x y));
 
 
 (* consts *)