Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add_notation: permissive about undeclared consts;
authorwenzelm
Tue, 05 Dec 2006 22:14:46 +0100
changeset 21661 e070569dd638
parent 21660 c86b761d6c06
child 21662 ab802d4eaaf4
add_notation: permissive about undeclared consts;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle