Tactic.norm_hhf;

--- a/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:13 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:27 2001 +0100
@@ -266,7 +266,7 @@
   end;
 
 val rulify =
-  standard o full_simplify [Drule.norm_hhf_eq] o
+  standard o Tactic.norm_hhf o
   full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
   full_simplify inductive_conj;