# HG changeset patch
# User berghofe
# Date 999267722 -7200
# Node ID b2e4077979b597aff5cc93a558d04e706fb11bcc
# Parent  a4651798a12af6efe23a6796a5443e3aa66da2a3
Removed tag_assumption.

diff -r a4651798a12a -r b2e4077979b5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Aug 31 16:21:31 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Aug 31 16:22:02 2001 +0200
@@ -852,7 +852,7 @@
     val (ctxt', [(_, thms)]) =
       ctxt
       |> auto_bind_facts name props
-      |> have_thmss [((name, attrs @ [Drule.tag_assumption]), ths)];
+      |> have_thmss [((name, attrs), ths)];
   in (ctxt', (cprops, (name, asms), (name, thms))) end;
 
 fun gen_assms prepp exp args ctxt =