changeset 26496 | 49ae9456eba9 |
parent 26411 | cd74690f3bfb |
child 27211 | 6724f31a1c8e |
--- a/src/FOL/cladata.ML Sat Mar 29 19:24:57 2008 +0100 +++ b/src/FOL/cladata.ML Sat Mar 29 22:55:49 2008 +0100 @@ -36,7 +36,7 @@ val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}] addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}]; -val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)); +val cla_setup = Cla.map_claset (K FOL_cs); val case_setup = (Method.add_methods