| changeset 18708 | 4b3dadb4fe33 |
| parent 18529 | 540da2415751 |
| child 20223 | 89d2758ecddf |
--- 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 ***)