src/FOL/simpdata.ML
changeset 18708 4b3dadb4fe33
parent 18529 540da2415751
child 20223 89d2758ecddf
     1.1 --- a/src/FOL/simpdata.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -361,7 +361,7 @@
     1.4  (*classical simprules too*)
     1.5  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
     1.6  
     1.7 -val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
     1.8 +val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
     1.9  
    1.10  
    1.11  (*** integration of simplifier with classical reasoner ***)