diff -r 9d6154f76476 -r 4b3dadb4fe33 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/FOL/simpdata.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -361,7 +361,7 @@
 (*classical simprules too*)
 val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
 
-val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
+val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
 
 
 (*** integration of simplifier with classical reasoner ***)