abbrevs: return result;

--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 09 18:58:52 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 09 21:44:27 2006 +0100
@@ -221,7 +221,7 @@
     (P.opt_locale_target -- opt_mode --
       Scan.repeat1 (Scan.option constdecl -- P.prop)
     >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.abbreviation mode args)));
+        Toplevel.local_theory loc (snd o Specification.abbreviation mode args)));
 
 val notationP =
   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl

--- a/src/Pure/Isar/proof_context.ML	Thu Nov 09 18:58:52 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 09 21:44:27 2006 +0100
@@ -140,8 +140,8 @@
   val expand_abbrevs: bool -> Proof.context -> Proof.context
   val add_notation: Syntax.mode -> (term * mixfix) list ->
     Proof.context -> Proof.context
-  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list ->
-    Proof.context -> Proof.context
+  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context ->
+    (term * term) list * Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
@@ -867,10 +867,11 @@
 
 val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
 
-fun add_abbrevs prmode = fold (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
+fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
   let
     val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt;
-    val c' = Syntax.constN ^ full_name ctxt c;
+    val full_c = full_name ctxt c;
+    val c' = Syntax.constN ^ full_c;
     val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t;
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val T = Term.fastype_of t;
@@ -883,6 +884,7 @@
     |> map_consts (apsnd
       (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true)))
     |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
+    |> pair (Const (full_c, T), t)
   end);
 
 

--- a/src/Pure/sign.ML	Thu Nov 09 18:58:52 2006 +0100
+++ b/src/Pure/sign.ML	Thu Nov 09 21:44:27 2006 +0100
@@ -192,7 +192,8 @@
   val read_prop: theory -> string -> term
   val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
   val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
-  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
+  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory ->
+    (term * term) list * theory
   include SIGN_THEORY
 end
 
@@ -752,20 +753,23 @@
 
 (* add abbreviations *)
 
-fun add_abbrevs (mode, inout) = fold (fn ((raw_c, raw_mx), raw_t) => fn thy =>
+fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn thy =>
   let
     val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
       Term.no_dummy_patterns o cert_term_abbrev thy;
 
     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-    val c' = Syntax.constN ^ full_name thy c;
+    val full_c = full_name thy c;
+    val c' = Syntax.constN ^ full_c;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val T = Term.fastype_of t;
   in
     thy
-    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true))
-    |> add_modesyntax_i (mode, inout) [(c', T, mx)]
+    |> map_consts
+      (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true))
+    |> add_modesyntax_i prmode [(c', T, mx)]
+    |> pair (Const (full_c, T), t)
   end);