--- 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, [])])];