# HG changeset patch
# User wenzelm
# Date 1165353286 -3600
# Node ID e070569dd638100a908c482aeb0b960d37e6a35d
# Parent  c86b761d6c066e0abc244ae66c1a49f13c32a948
add_notation: permissive about undeclared consts;

diff -r c86b761d6c06 -r e070569dd638 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Dec 05 22:14:45 2006 +0100
+++ b/src/Pure/sign.ML	Tue Dec 05 22:14:46 2006 +0100
@@ -714,7 +714,7 @@
 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 const_syntax thy (Const (c, _), mx) = SOME (Consts.syntax (consts_of thy) (c, mx))
+fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
   | const_syntax _ _ = NONE;
 
 fun add_notation mode args thy =
@@ -751,7 +751,7 @@
 end;
 
 
-(* add abbreviations *)
+(* add abbreviations -- cf. Sign.add_abbrevs *)
 
 fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
   let