generalized notation interface (add or del);

--- a/src/Pure/Isar/class.ML	Wed Oct 10 17:31:55 2007 +0200
+++ b/src/Pure/Isar/class.ML	Wed Oct 10 17:31:56 2007 +0200
@@ -800,7 +800,7 @@
     val ty' = fastype_of rhs';
   in
     thy
-    |> Sign.add_notation prmode [(Const (c', ty'), syn)]
+    |> Sign.notation true prmode [(Const (c', ty'), syn)]
     |> register_abbrev class (c', ty')
     |> pair c'
   end;

--- a/src/Pure/Isar/local_theory.ML	Wed Oct 10 17:31:55 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Oct 10 17:31:56 2007 +0200
@@ -36,7 +36,7 @@
   val declaration: declaration -> local_theory -> local_theory
   val note: string -> (bstring * Attrib.src list) * thm list ->
     local_theory -> (bstring * thm list) * local_theory
-  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val target_naming: local_theory -> NameSpace.naming
   val target_name: local_theory -> bstring -> string
@@ -167,9 +167,9 @@
   ProofContext.export_morphism lthy (target_of lthy) $>
   Morphism.thm_morphism Goal.norm_result;
 
-fun notation mode raw_args lthy =
+fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
-  in term_syntax (ProofContext.target_notation mode args) lthy end;
+  in term_syntax (ProofContext.target_notation add mode args) lthy end;
 
 val target_name = NameSpace.full o target_naming;
 

--- a/src/Pure/Isar/proof_context.ML	Wed Oct 10 17:31:55 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Oct 10 17:31:56 2007 +0200
@@ -139,9 +139,8 @@
   val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
   val get_case: Proof.context -> string -> string option list -> RuleCases.T
-  val add_notation: Syntax.mode -> (term * mixfix) list ->
-    Proof.context -> Proof.context
-  val target_notation: Syntax.mode -> (term * mixfix) list -> morphism ->
+  val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
+  val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> Markup.property list ->
@@ -991,11 +990,6 @@
 
 (* authentic constants *)
 
-fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
-  | const_syntax ctxt (Const (c, _), mx) =
-      Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
-  | const_syntax _ _ = NONE;
-
 fun context_const_ast_tr ctxt [Syntax.Variable c] =
       let
         val consts = consts_of ctxt;
@@ -1013,13 +1007,24 @@
 
 (* notation *)
 
-fun add_notation mode args ctxt =
-  ctxt |> map_syntax
-    (LocalSyntax.add_modesyntax (theory_of ctxt) mode (map_filter (const_syntax ctxt) args));
+local
+
+fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
+  | const_syntax ctxt (Const (c, _), mx) =
+      Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
+  | const_syntax _ _ = NONE;
+
+in
 
-fun target_notation mode args phi =
+fun notation add mode args ctxt =
+  ctxt |> map_syntax
+    (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
+
+fun target_notation add mode args phi =
   let val args' = filter (fn (t, _) => Term.equiv_types (t, Morphism.term phi t)) args;
-  in Context.mapping (Sign.add_notation mode args') (add_notation mode args') end;
+  in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
+
+end;
 
 
 (* local constants *)

--- a/src/Pure/Isar/specification.ML	Wed Oct 10 17:31:55 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Oct 10 17:31:56 2007 +0200
@@ -42,8 +42,8 @@
     local_theory -> local_theory
   val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
     local_theory -> local_theory
-  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val notation_cmd: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
     -> local_theory -> (bstring * thm list) list * local_theory
   val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
@@ -221,8 +221,8 @@
 
 (* notation *)
 
-fun gen_notation prep_const mode args lthy =
-  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
+fun gen_notation prep_const add mode args lthy =
+  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation (K I);
 val notation_cmd = gen_notation ProofContext.read_const;

--- a/src/Pure/Isar/theory_target.ML	Wed Oct 10 17:31:55 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Oct 10 17:31:56 2007 +0200
@@ -175,7 +175,7 @@
       (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg')
     #-> (fn (lhs, _) =>
       Term.equiv_types (rhs, rhs') ?
-        Morphism.form (ProofContext.target_notation prmode [(lhs, mx)])))
+        Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)])))
   end;
 
 fun internal_abbrev loc prmode ((c, mx), t) lthy = lthy
@@ -279,10 +279,11 @@
     lthy
     |> LocalTheory.theory_result
         (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
-    |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)])
-    #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
-    #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
-    #> local_abbrev (c, rhs))
+    |-> (fn (lhs as Const (full_c, _), rhs) =>
+          LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
+          #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
+          #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
+          #> local_abbrev (c, rhs))
   end;
 
 

--- a/src/Pure/sign.ML	Wed Oct 10 17:31:55 2007 +0200
+++ b/src/Pure/sign.ML	Wed Oct 10 17:31:56 2007 +0200
@@ -158,7 +158,7 @@
   val read_prop: theory -> string -> term
   val add_consts_authentic: Markup.property list ->
     (bstring * typ * mixfix) list -> theory -> theory
-  val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
+  val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrev: string -> Markup.property list ->
     bstring * term -> theory -> (term * term) * theory
   include SIGN_THEORY
@@ -665,8 +665,8 @@
 fun const_syntax thy (Const (c, _), mx) = try (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);
+fun notation add mode args thy = thy
+  |> (if add then add_modesyntax_i else del_modesyntax_i) mode (map_filter (const_syntax thy) args);
 
 
 (* add constants *)