--- a/src/Pure/Isar/proof_context.ML Thu Dec 07 17:58:45 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Dec 07 17:58:46 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: Syntax.mode -> ((bstring * mixfix) * term) list -> Proof.context ->
- (term * term) list * Proof.context
+ val add_abbrevs: string -> (bstring * term) list -> Proof.context ->
+ ((string * typ) * term) list * Proof.context
val verbose: bool ref
val setmp_verbose: ('a -> 'b) -> 'a -> 'b
val print_syntax: Proof.context -> unit
@@ -877,21 +877,18 @@
val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
-fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
+fun add_abbrevs mode = fold_map (fn (c, raw_t) => fn ctxt =>
let
- val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
val t0 = cert_term (ctxt |> expand_abbrevs false) 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 (((full_c, T), rhs), consts') = consts_of ctxt
- |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true);
+ val (res, consts') = consts_of ctxt
+ |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode ((c, t), true);
in
ctxt
|> Variable.declare_term t
|> map_consts (apsnd (K consts'))
- |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt)
- prmode [(false, (Syntax.constN ^ full_c, T, mx))])
- |> pair (Const (full_c, T), rhs)
+ |> pair res
end);