# HG changeset patch
# User wenzelm
# Date 1165522128 -3600
# Node ID f4fe6e5a3ee692c07ce1d329b9b0cb8af6cff1ec
# Parent  a9fdad55a53d832fef41bb97ca373fd651d66938
simplified add_abbrev -- single argument;

diff -r a9fdad55a53d -r f4fe6e5a3ee6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Dec 07 21:08:45 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Dec 07 21:08:48 2006 +0100
@@ -142,8 +142,8 @@
   val add_notation: Syntax.mode -> (term * mixfix) list ->
     Proof.context -> Proof.context
   val expand_abbrevs: bool -> Proof.context -> Proof.context
-  val add_abbrevs: string -> (bstring * term) list -> Proof.context ->
-    ((string * typ) * term) list * Proof.context
+  val add_abbrev: string -> bstring * term -> Proof.context ->
+    ((string * typ) * term) * Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
@@ -877,7 +877,7 @@
 
 val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
 
-fun add_abbrevs mode = fold_map (fn (c, raw_t) => fn ctxt =>
+fun add_abbrev mode (c, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
@@ -889,7 +889,7 @@
     |> Variable.declare_term t
     |> map_consts (apsnd (K consts'))
     |> pair res
-  end);
+  end;
 
 
 (* fixes *)
diff -r a9fdad55a53d -r f4fe6e5a3ee6 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Dec 07 21:08:45 2006 +0100
+++ b/src/Pure/sign.ML	Thu Dec 07 21:08:48 2006 +0100
@@ -192,8 +192,7 @@
   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: string -> (bstring * term) list -> theory ->
-    ((string * typ) * term) list * theory
+  val add_abbrev: string -> bstring * term -> theory -> ((string * typ) * term) * theory
   include SIGN_THEORY
 end
 
@@ -753,14 +752,14 @@
 
 (* add abbreviations *)
 
-fun add_abbrevs mode = fold_map (fn (c, raw_t) => fn thy =>
+fun add_abbrev mode (c, raw_t) thy =
   let
     val prep_tm = Compress.term thy o Term.no_dummy_patterns o cert_term_abbrev thy;
     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 (res, consts') = consts_of thy
       |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true);
-  in (res, thy |> map_consts (K consts')) end);
+  in (res, thy |> map_consts (K consts')) end;
 
 
 (* add constraints *)