--- a/src/Pure/Isar/proof_context.ML Wed Dec 06 21:18:57 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Dec 06 21:18:58 2006 +0100
@@ -139,9 +139,9 @@
val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
val get_case: Proof.context -> string -> string option list -> RuleCases.T
- val expand_abbrevs: bool -> Proof.context -> Proof.context
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 verbose: bool ref
@@ -880,22 +880,18 @@
fun add_abbrevs prmode = fold_map (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
let
val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
- val _ = no_skolem true 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 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 T = Term.fastype_of t;
- val _ =
- if null (Variable.hidden_polymorphism t T) then ()
- else error ("Extra type variables on rhs of abbreviation: " ^ quote c);
+ val (((full_c, T), rhs), consts') = consts_of ctxt
+ |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true);
in
ctxt
|> Variable.declare_term t
- |> 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)
+ |> 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)
end);