--- a/src/Pure/sign.ML Wed Dec 06 21:18:57 2006 +0100
+++ b/src/Pure/sign.ML Wed Dec 06 21:18:58 2006 +0100
@@ -751,25 +751,21 @@
end;
-(* add abbreviations -- cf. Sign.add_abbrevs *)
+(* add abbreviations -- cf. ProofContext.add_abbrevs *)
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 full_c = full_name thy c;
- val c' = Syntax.constN ^ full_c;
+ 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 T = Term.fastype_of t;
+ val (((full_c, T), rhs), consts') = consts_of thy
+ |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) (#1 prmode) ((c, t), true);
in
thy
- |> 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)
+ |> map_consts (K consts')
+ |> add_modesyntax_i prmode [(Syntax.constN ^ full_c, T, mx)]
+ |> pair (Const (full_c, T), rhs)
end);