diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -622,7 +622,7 @@
 
 val local_results = gen_thmss ProofContext.note_thmss_i (K []) I I (K I);
 fun global_results kind =
-  swap oo (PureThy.note_thmss_i (Drule.kind kind) o map (apsnd Thm.simple_fact));
+  PureThy.note_thmss_i (Drule.kind kind) o map (apsnd Thm.simple_fact);
 
 fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
 fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];