src/Pure/sign.ML
changeset 21269 c605503bb4ef
parent 21206 2af4c7b3f7ef
child 21661 e070569dd638
     1.1 --- a/src/Pure/sign.ML	Thu Nov 09 18:58:52 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 09 21:44:27 2006 +0100
     1.3 @@ -192,7 +192,8 @@
     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: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
     1.8 +  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory ->
     1.9 +    (term * term) list * theory
    1.10    include SIGN_THEORY
    1.11  end
    1.12  
    1.13 @@ -752,20 +753,23 @@
    1.14  
    1.15  (* add abbreviations *)
    1.16  
    1.17 -fun add_abbrevs (mode, inout) = fold (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    1.18 +fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    1.19    let
    1.20      val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
    1.21        Term.no_dummy_patterns o cert_term_abbrev thy;
    1.22  
    1.23      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.24 -    val c' = Syntax.constN ^ full_name thy c;
    1.25 +    val full_c = full_name thy c;
    1.26 +    val c' = Syntax.constN ^ full_c;
    1.27      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.28        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.29      val T = Term.fastype_of t;
    1.30    in
    1.31      thy
    1.32 -    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true))
    1.33 -    |> add_modesyntax_i (mode, inout) [(c', T, mx)]
    1.34 +    |> map_consts
    1.35 +      (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true))
    1.36 +    |> add_modesyntax_i prmode [(c', T, mx)]
    1.37 +    |> pair (Const (full_c, T), t)
    1.38    end);
    1.39  
    1.40