# HG changeset patch
# User wenzelm
# Date 1147807994 -7200
# Node ID baab85f25e0edcf938576893a0b5de91d4b2a113
# Parent  e3ec6839c631222c6cf54cedf8e42b56be775646
added syntax interface;
tuned interface;

diff -r e3ec6839c631 -r baab85f25e0e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue May 16 21:33:11 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue May 16 21:33:14 2006 +0200
@@ -24,6 +24,8 @@
   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 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
   val consts_restricted: (string * typ -> bool) ->
     ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
@@ -41,7 +43,6 @@
   val def_finish: (local_theory -> term -> thm -> thm) ->
     (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     local_theory -> (term * (bstring * thm)) * local_theory
-  val abbrev: string * bool -> (bstring * mixfix) * term -> local_theory -> local_theory
 end;
 
 structure LocalTheory: LOCAL_THEORY =
@@ -164,6 +165,22 @@
 
 (** local theory **)
 
+(* term syntax *)
+
+fun term_syntax add_thy add_ctxt prmode args ctxt = ctxt |>
+  (case locale_of ctxt of
+    NONE => theory (add_thy prmode args)
+  | SOME (loc, _) =>
+      locale (Locale.add_term_syntax loc (add_ctxt prmode args)) #>
+      add_ctxt prmode args);
+
+val syntax = term_syntax Sign.add_const_syntax ProofContext.add_const_syntax;
+
+fun abbrevs prmode args =
+  term_syntax Sign.add_abbrevs ProofContext.add_abbrevs
+    prmode (map (fn ((x, mx), rhs) => (x, rhs, mx)) args);
+
+
 (* consts *)
 
 fun consts_restricted pred decls ctxt =
@@ -172,18 +189,16 @@
     val params = filter pred (params_of ctxt);
     val ps = map Free params;
     val Ps = map #2 params;
-    val abbrevs = decls |> map (fn ((c, T), mx) =>
-      let val t = Term.list_comb (Const (Sign.full_name thy c, Ps ---> T), ps)
-      in (c, t, mx) end);
+    val abbrs = decls |> map (fn ((c, T), mx) =>
+      ((c, mx), Term.list_comb (Const (Sign.full_name thy c, Ps ---> T), ps)));
   in
     ctxt |>
     (case locale_of ctxt of
-      NONE => theory (Sign.add_consts_i (map (fn ((c, T), mx) => (c, T, mx)) decls))
+      NONE => theory (Sign.add_consts_authentic (map (fn ((c, T), mx) => (c, T, mx)) decls))
     | SOME (loc, _) =>
         theory (Sign.add_consts_i (map (fn ((c, T), _) => (c, Ps ---> T, NoSyn)) decls)) #>
-        locale (Locale.add_abbrevs loc Syntax.default_mode abbrevs) #>
-        ProofContext.add_abbrevs_i Syntax.default_mode abbrevs)
-    |> pair (map #2 abbrevs)
+        abbrevs Syntax.default_mode abbrs)
+    |> pair (map #2 abbrs)
   end;
 
 val consts = consts_restricted (K true);
@@ -277,18 +292,4 @@
 
 end;
 
-
-(* constant abbreviations *)
-
-fun abbrev prmode ((x, mx), rhs) ctxt =
-  let val abbrevs = [(x, rhs, mx)] in
-    ctxt |>
-    (case locale_of ctxt of
-      NONE =>
-        theory (Sign.add_abbrevs_i prmode abbrevs)
-    | SOME (loc, _) =>
-        locale (Locale.add_abbrevs loc prmode abbrevs) #>
-        ProofContext.add_abbrevs_i prmode abbrevs)
-  end;
-
 end;