src/Pure/Isar/proof.ML
changeset 13297 e4ae0732e2be
parent 13277 ca2511db144d
child 13335 7995b3f4ca5e
--- a/src/Pure/Isar/proof.ML	Thu Jul 04 15:06:46 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 04 16:48:21 2002 +0200
@@ -249,7 +249,7 @@
 val reset_facts = put_facts None;
 
 fun these_factss (state, named_factss) =
-  state |> put_facts (Some (flat (map #2 named_factss)));
+  state |> put_facts (Some (flat (map snd named_factss)));
 
 
 (* goal *)