# HG changeset patch
# User wenzelm
# Date 1025617262 -7200
# Node ID ca2511db144dbe7e01768700e10aa3eef0b2545f
# Parent  a02ee4fec6b777fe5352ee3494855f149e638190
these_facts: refrain from put_thmss (2nd time!);

diff -r a02ee4fec6b7 -r ca2511db144d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 02 15:40:27 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 02 15:41:02 2002 +0200
@@ -249,9 +249,7 @@
 val reset_facts = put_facts None;
 
 fun these_factss (state, named_factss) =
-  state
-  |> put_thmss named_factss
-  |> put_facts (Some (flat (map #2 named_factss)));
+  state |> put_facts (Some (flat (map #2 named_factss)));
 
 
 (* goal *)