# HG changeset patch
# User wenzelm
# Date 1165955113 -3600
# Node ID a59f083632a7a9ea84efe619941d30922d86ca1a
# Parent  6086783d42146637db5a2eb108e6bad8564f02cb
add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);

diff -r 6086783d4214 -r a59f083632a7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Dec 12 20:50:23 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Dec 12 21:25:13 2006 +0100
@@ -899,14 +899,12 @@
     val t0 = cert_term (ctxt |> set_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 ((lhs as Const (full_c, T), rhs), consts') = consts_of ctxt
+    val ((lhs, rhs), consts') = consts_of ctxt
       |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (c, t);
-    val get = fn Const (c', _) => if c' = full_c then SOME (T, rhs) else NONE | _ => NONE;
   in
     ctxt
     |> map_consts (apsnd (K consts'))
     |> Variable.declare_term rhs
-    |> Assumption.add_assms (K (K (I, Envir.expand_term get))) [] |> snd
     |> pair (lhs, rhs)
   end;