--- a/src/HOL/List.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/List.ML Sun Oct 14 22:08:29 2001 +0200
@@ -413,7 +413,7 @@
by Auto_tac;
qed "rev_exhaust_aux";
-bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux);
+bind_thm ("rev_exhaust", ObjectLogic.rulify rev_exhaust_aux);
(** set **)