# HG changeset patch
# User haftmann
# Date 1164990152 -3600
# Node ID 5825a59785f4d3d2e0c9fc9a4747340a3e70e6aa
# Parent  f9fd69d96c4e0626be5026bc21f1f96f74d41cf1
made SML/NJ happy

diff -r f9fd69d96c4e -r 5825a59785f4 src/Pure/Isar/proof_context.ML
--- 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;