src/Pure/sign.ML
changeset 24776 38afb780f622
parent 24761 d762ab297a07
child 24921 708b2f887a42
     1.1 --- a/src/Pure/sign.ML	Sun Sep 30 16:20:37 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Sep 30 16:20:38 2007 +0200
     1.3 @@ -161,9 +161,11 @@
     1.4    val simple_read_term: theory -> typ -> string -> term
     1.5    val read_term: theory -> string -> term
     1.6    val read_prop: theory -> string -> term
     1.7 -  val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
     1.8 +  val add_consts_authentic: Markup.property list ->
     1.9 +    (bstring * typ * mixfix) list -> theory -> theory
    1.10    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.11 -  val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
    1.12 +  val add_abbrev: string -> Markup.property list ->
    1.13 +    bstring * term -> theory -> (term * term) * theory
    1.14    include SIGN_THEORY
    1.15    val add_const_constraint: string * typ option -> theory -> theory
    1.16    val primitive_class: string * class list -> theory -> theory
    1.17 @@ -694,7 +696,7 @@
    1.18  
    1.19  local
    1.20  
    1.21 -fun gen_add_consts prep_typ authentic raw_args thy =
    1.22 +fun gen_add_consts prep_typ authentic tags raw_args thy =
    1.23    let
    1.24      val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    1.25      fun prep (raw_c, raw_T, raw_mx) =
    1.26 @@ -703,18 +705,18 @@
    1.27          val c' = if authentic then Syntax.constN ^ full_name thy c else c;
    1.28          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.29            cat_error msg ("in declaration of constant " ^ quote c);
    1.30 -      in (((c, T), authentic), (c', T, mx)) end;
    1.31 +      in ((c, T), (c', T, mx)) end;
    1.32      val args = map prep raw_args;
    1.33    in
    1.34      thy
    1.35 -    |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
    1.36 +    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
    1.37      |> add_syntax_i (map #2 args)
    1.38    end;
    1.39  
    1.40  in
    1.41  
    1.42 -val add_consts = gen_add_consts read_typ false;
    1.43 -val add_consts_i = gen_add_consts certify_typ false;
    1.44 +val add_consts = gen_add_consts read_typ false [];
    1.45 +val add_consts_i = gen_add_consts certify_typ false [];
    1.46  val add_consts_authentic = gen_add_consts certify_typ true;
    1.47  
    1.48  end;
    1.49 @@ -722,7 +724,7 @@
    1.50  
    1.51  (* add abbreviations *)
    1.52  
    1.53 -fun add_abbrev mode (c, raw_t) thy =
    1.54 +fun add_abbrev mode tags (c, raw_t) thy =
    1.55    let
    1.56      val pp = pp thy;
    1.57      val prep_tm = Compress.term thy o no_frees pp o
    1.58 @@ -731,7 +733,7 @@
    1.59      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.60        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.61      val (res, consts') = consts_of thy
    1.62 -      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (c, t);
    1.63 +      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
    1.64    in (res, thy |> map_consts (K consts')) end;
    1.65  
    1.66