Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
these_facts: refrain from put_thmss (2nd time!);
authorwenzelm
Tue, 02 Jul 2002 15:41:02 +0200
changeset 13277 ca2511db144d
parent 13276 a02ee4fec6b7
child 13278 b62514fcbcab
these_facts: refrain from put_thmss (2nd time!);
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle