# HG changeset patch
# User wenzelm
# Date 938727073 -7200
# Node ID 80c310e76c46ca7188a35312e090f49499db63c3
# Parent  22dc8b2455b827e6634062ee6dacdb7f8b5e12bd
removed ProofContext.declare_thm;

diff -r 22dc8b2455b8 -r 80c310e76c46 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Sep 30 21:23:08 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Sep 30 23:31:13 1999 +0200
@@ -214,7 +214,7 @@
     val (xs, ss) = Library.split_list insts;
     val Ts = map get_typ xs;
 
-    val (ts, envT) = ProofContext.read_termTs (ctxt |> ProofContext.declare_thm thm) (ss ~~ Ts);
+    val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts);
     val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
     val cenv =
       map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))