| changeset 31902 | 862ae16a799d |
| parent 30515 | bca05b17b618 |
| child 33002 | f3f02f36a3e2 |
--- a/src/Tools/atomize_elim.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/Tools/atomize_elim.ML Thu Jul 02 17:34:14 2009 +0200 @@ -20,7 +20,9 @@ struct (* theory data *) -structure AtomizeElimData = NamedThmsFun( + +structure AtomizeElimData = Named_Thms +( val name = "atomize_elim"; val description = "atomize_elim rewrite rule"; );