rev_exhaust: rulify;

--- a/src/HOL/List.ML	Fri Nov 03 21:31:53 2000 +0100
+++ b/src/HOL/List.ML	Fri Nov 03 21:32:41 2000 +0100
@@ -417,8 +417,9 @@
 Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
 by (rev_induct_tac "xs" 1);
 by Auto_tac;
-bind_thm ("rev_exhaust",
-  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
+qed "rev_exhaust_aux";
+
+bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux);
 
 
 (** set **)