# HG changeset patch
# User wenzelm
# Date 1162896408 -3600
# Node ID 2af4c7b3f7ef6a20c7e703a627acd84350b1e28e
# Parent  dfe338ec9f9ca482bbbe226a796aba86eaecd088
replaced const_syntax by notation, which operates on terms;

diff -r dfe338ec9f9c -r 2af4c7b3f7ef src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Nov 07 11:46:47 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Tue Nov 07 11:46:48 2006 +0100
@@ -33,7 +33,7 @@
     local_theory -> (term * (bstring * thm)) * local_theory
   val note: (bstring * Attrib.src list) * thm list ->
     local_theory -> (bstring * thm list) * Proof.context
-  val const_syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
   val init: string option -> operations -> Proof.context -> local_theory
   val reinit: local_theory -> local_theory
@@ -153,12 +153,11 @@
 
 fun note (a, ths) lthy = lthy |> notes [(a, [(ths, [])])] |>> hd;
 
-fun const_syntax mode args =
-  term_syntax
-    (Context.mapping (Sign.add_const_syntax mode args) (ProofContext.add_const_syntax mode args));
+fun notation mode args = term_syntax
+  (Context.mapping (Sign.add_notation mode args) (ProofContext.add_notation mode args));
 
-fun abbrevs mode args =
-  term_syntax (Context.mapping (Sign.add_abbrevs mode args) (ProofContext.add_abbrevs mode args));
+fun abbrevs mode args = term_syntax
+  (Context.mapping (Sign.add_abbrevs mode args) (ProofContext.add_abbrevs mode args));
 
 
 (* init -- exit *)
diff -r dfe338ec9f9c -r 2af4c7b3f7ef src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Nov 07 11:46:47 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Nov 07 11:46:48 2006 +0100
@@ -34,8 +34,8 @@
     local_theory -> local_theory
   val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
     local_theory -> local_theory
-  val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
-  val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
     -> local_theory -> (bstring * thm list) list * local_theory
   val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
@@ -174,12 +174,11 @@
 
 (* const syntax *)
 
-fun gen_syntax intern_const mode raw_args lthy =
-  let val args = raw_args |> map (apfst (intern_const (ProofContext.consts_of lthy)))
-  in lthy |> LocalTheory.const_syntax mode args end;
+fun gen_notation prep_const mode args lthy =
+  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
 
-val const_syntax = gen_syntax Consts.intern;
-val const_syntax_i = gen_syntax (K I);
+val notation = gen_notation ProofContext.read_const;
+val notation_i = gen_notation (K I);
 
 
 (* fact statements *)
@@ -220,7 +219,7 @@
   let
     val _ = LocalTheory.assert lthy0;
     val thy = ProofContext.theory_of lthy0;
-    
+
     val (loc, ctxt, lthy) =
       (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
         (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
diff -r dfe338ec9f9c -r 2af4c7b3f7ef src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 07 11:46:47 2006 +0100
+++ b/src/Pure/sign.ML	Tue Nov 07 11:46:48 2006 +0100
@@ -191,7 +191,7 @@
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
   val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
-  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> theory -> theory
+  val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
   include SIGN_THEORY
 end
@@ -713,8 +713,11 @@
 val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
 
-fun add_const_syntax mode args thy =
-  thy |> add_modesyntax_i mode (map (Consts.syntax (consts_of thy)) args);
+fun const_syntax thy (Const (c, _), mx) = SOME (Consts.syntax (consts_of thy) (c, mx))
+  | const_syntax _ _ = NONE;
+
+fun add_notation mode args thy =
+  thy |> add_modesyntax_i mode (map_filter (const_syntax thy) args);
 
 
 (* add constants *)