# HG changeset patch
# User wenzelm
# Date 1191162040 -7200
# Node ID 3e7f71caae189b5c82e19234ac28b2c2ada2f57a
# Parent  c1250851d701a2b4f41bfcb3730a43325b5557e5
add_abbrev: tags (Markup.property list);

diff -r c1250851d701 -r 3e7f71caae18 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 30 16:20:39 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 30 16:20:40 2007 +0200
@@ -150,7 +150,8 @@
   val target_notation: Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
-  val add_abbrev: string -> bstring * term -> Proof.context -> (term * term) * Proof.context
+  val add_abbrev: string -> Markup.property list ->
+    bstring * term -> Proof.context -> (term * term) * Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
@@ -1021,13 +1022,13 @@
       in cert_term ctxt (Const (c, T)); T end;
   in ctxt |> map_consts (apsnd (Consts.constrain (c, Option.map prepT opt_T))) end;
 
-fun add_abbrev mode (c, raw_t) ctxt =
+fun add_abbrev mode tags (c, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
-      |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (c, t);
+      |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t);
   in
     ctxt
     |> map_consts (apsnd (K consts'))