| changeset 21622 | 5825a59785f4 |
| parent 21612 | 52859439959a |
| child 21643 | bdf3e74727df |
--- a/src/Pure/Isar/proof_context.ML Fri Dec 01 17:22:31 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Dec 01 17:22:32 2006 +0100 @@ -806,8 +806,8 @@ in -val note_thmss = gen_note_thmss get_thms; -val note_thmss_i = gen_note_thmss (K I); +fun note_thmss k = gen_note_thmss get_thms k; +fun note_thmss_i k = gen_note_thmss (K I) k; end;