author | wenzelm |
Tue, 02 Jul 2002 15:41:02 +0200 | |
changeset 13277 | ca2511db144d |
parent 13276 | a02ee4fec6b7 |
child 13278 | b62514fcbcab |
--- 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 *)