declare_const: Name.binding, store/report position;
authorwenzelm
Wed Sep 03 17:47:34 2008 +0200 (2008-09-03)
changeset 28111ea22fd4685fb
parent 28110 9d121b171a0a
child 28112 691993ef6abe
declare_const: Name.binding, store/report position;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Sep 03 17:47:30 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Sep 03 17:47:34 2008 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.7 -  val declare_const: Properties.T -> bstring * typ * mixfix -> theory -> term * theory
     1.8 +  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
     1.9    val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
    1.10    val revert_abbrev: string -> string -> theory -> theory
    1.11    val add_const_constraint: string * typ option -> theory -> theory
    1.12 @@ -527,7 +527,14 @@
    1.13  val add_consts = snd oo gen_add_consts Syntax.parse_typ false [];
    1.14  val add_consts_i = snd oo gen_add_consts (K I) false [];
    1.15  
    1.16 -fun declare_const tags arg = gen_add_consts (K I) true tags [arg] #>> the_single;
    1.17 +fun declare_const tags ((b, T), mx) thy =
    1.18 +  let
    1.19 +    val c = Name.name_of b;
    1.20 +    val pos = Name.pos_of b;
    1.21 +    val tags' = Position.default_properties pos tags;
    1.22 +    val ([const as Const (full_c, _)], thy') = gen_add_consts (K I) true tags' [(c, T, mx)] thy;
    1.23 +    val _ = Position.report (Markup.const_decl full_c) pos;
    1.24 +  in (const, thy') end;
    1.25  
    1.26  end;
    1.27