abbrevs: return result;
authorwenzelm
Thu Nov 09 21:44:27 2006 +0100 (2006-11-09)
changeset 21269c605503bb4ef
parent 21268 7a6299a17386
child 21270 b82f4c16355e
abbrevs: return result;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 09 18:58:52 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 09 21:44:27 2006 +0100
     1.3 @@ -221,7 +221,7 @@
     1.4      (P.opt_locale_target -- opt_mode --
     1.5        Scan.repeat1 (Scan.option constdecl -- P.prop)
     1.6      >> (fn ((loc, mode), args) =>
     1.7 -        Toplevel.local_theory loc (Specification.abbreviation mode args)));
     1.8 +        Toplevel.local_theory loc (snd o Specification.abbreviation mode args)));
     1.9  
    1.10  val notationP =
    1.11    OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Nov 09 18:58:52 2006 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 09 21:44:27 2006 +0100
     2.3 @@ -140,8 +140,8 @@
     2.4    val expand_abbrevs: bool -> Proof.context -> Proof.context
     2.5    val add_notation: Syntax.mode -> (term * mixfix) list ->
     2.6      Proof.context -> Proof.context
     2.7 -  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list ->
     2.8 -    Proof.context -> Proof.context
     2.9 +  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context ->
    2.10 +    (term * term) list * Proof.context
    2.11    val verbose: bool ref
    2.12    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    2.13    val print_syntax: Proof.context -> unit
    2.14 @@ -867,10 +867,11 @@
    2.15  
    2.16  val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
    2.17  
    2.18 -fun add_abbrevs prmode = fold (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
    2.19 +fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
    2.20    let
    2.21      val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt;
    2.22 -    val c' = Syntax.constN ^ full_name ctxt c;
    2.23 +    val full_c = full_name ctxt c;
    2.24 +    val c' = Syntax.constN ^ full_c;
    2.25      val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t;
    2.26      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
    2.27      val T = Term.fastype_of t;
    2.28 @@ -883,6 +884,7 @@
    2.29      |> map_consts (apsnd
    2.30        (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true)))
    2.31      |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
    2.32 +    |> pair (Const (full_c, T), t)
    2.33    end);
    2.34  
    2.35  
     3.1 --- a/src/Pure/sign.ML	Thu Nov 09 18:58:52 2006 +0100
     3.2 +++ b/src/Pure/sign.ML	Thu Nov 09 21:44:27 2006 +0100
     3.3 @@ -192,7 +192,8 @@
     3.4    val read_prop: theory -> string -> term
     3.5    val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
     3.6    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
     3.7 -  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
     3.8 +  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory ->
     3.9 +    (term * term) list * theory
    3.10    include SIGN_THEORY
    3.11  end
    3.12  
    3.13 @@ -752,20 +753,23 @@
    3.14  
    3.15  (* add abbreviations *)
    3.16  
    3.17 -fun add_abbrevs (mode, inout) = fold (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    3.18 +fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    3.19    let
    3.20      val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
    3.21        Term.no_dummy_patterns o cert_term_abbrev thy;
    3.22  
    3.23      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    3.24 -    val c' = Syntax.constN ^ full_name thy c;
    3.25 +    val full_c = full_name thy c;
    3.26 +    val c' = Syntax.constN ^ full_c;
    3.27      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    3.28        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    3.29      val T = Term.fastype_of t;
    3.30    in
    3.31      thy
    3.32 -    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true))
    3.33 -    |> add_modesyntax_i (mode, inout) [(c', T, mx)]
    3.34 +    |> map_consts
    3.35 +      (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true))
    3.36 +    |> add_modesyntax_i prmode [(c', T, mx)]
    3.37 +    |> pair (Const (full_c, T), t)
    3.38    end);
    3.39  
    3.40