Removed tag_assumption.
authorberghofe
Fri, 31 Aug 2001 16:22:02 +0200
changeset 11526 b2e4077979b5
parent 11525 a4651798a12a
child 11527 4db3876f1224
Removed tag_assumption.
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 =