src/Pure/sign.ML
changeset 21661 e070569dd638
parent 21269 c605503bb4ef
child 21681 8b8edcdb4da8
     1.1 --- a/src/Pure/sign.ML	Tue Dec 05 22:14:45 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 05 22:14:46 2006 +0100
     1.3 @@ -714,7 +714,7 @@
     1.4  val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
     1.5  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
     1.6  
     1.7 -fun const_syntax thy (Const (c, _), mx) = SOME (Consts.syntax (consts_of thy) (c, mx))
     1.8 +fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
     1.9    | const_syntax _ _ = NONE;
    1.10  
    1.11  fun add_notation mode args thy =
    1.12 @@ -751,7 +751,7 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* add abbreviations *)
    1.17 +(* add abbreviations -- cf. Sign.add_abbrevs *)
    1.18  
    1.19  fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    1.20    let