Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/sign.ML
changeset 24949 5f00e3532418
parent 24921 708b2f887a42
child 24959 119793c84647 
--- 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 *)
isabelle