src/Pure/sign.ML
changeset 21704 f4fe6e5a3ee6
parent 21696 f3c78a133fbb
child 21722 25239591e732
     1.1 --- a/src/Pure/sign.ML	Thu Dec 07 21:08:45 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Dec 07 21:08:48 2006 +0100
     1.3 @@ -192,8 +192,7 @@
     1.4    val read_prop: theory -> string -> term
     1.5    val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
     1.6    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.7 -  val add_abbrevs: string -> (bstring * term) list -> theory ->
     1.8 -    ((string * typ) * term) list * theory
     1.9 +  val add_abbrev: string -> bstring * term -> theory -> ((string * typ) * term) * theory
    1.10    include SIGN_THEORY
    1.11  end
    1.12  
    1.13 @@ -753,14 +752,14 @@
    1.14  
    1.15  (* add abbreviations *)
    1.16  
    1.17 -fun add_abbrevs mode = fold_map (fn (c, raw_t) => fn thy =>
    1.18 +fun add_abbrev mode (c, raw_t) thy =
    1.19    let
    1.20      val prep_tm = Compress.term thy o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.21      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.22        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.23      val (res, consts') = consts_of thy
    1.24        |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true);
    1.25 -  in (res, thy |> map_consts (K consts')) end);
    1.26 +  in (res, thy |> map_consts (K consts')) end;
    1.27  
    1.28  
    1.29  (* add constraints *)