src/HOL/List.ML
changeset 11770 b6bb7a853dd2
parent 11701 3d51fbf81c17
child 11868 56db9f3a6b3e
     1.1 --- a/src/HOL/List.ML	Sun Oct 14 22:07:01 2001 +0200
     1.2 +++ b/src/HOL/List.ML	Sun Oct 14 22:08:29 2001 +0200
     1.3 @@ -413,7 +413,7 @@
     1.4  by Auto_tac;
     1.5  qed "rev_exhaust_aux";
     1.6  
     1.7 -bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux);
     1.8 +bind_thm ("rev_exhaust", ObjectLogic.rulify rev_exhaust_aux);
     1.9  
    1.10  
    1.11  (** set **)