diff -r e280491f36b8 -r 862ae16a799d src/Tools/atomize_elim.ML
--- 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";
 );