diff -r ba142aa29694 -r e4ae0732e2be src/Pure/Isar/proof.ML
--- 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 *)