src/HOL/Tools/inductive_package.ML

       | _ => err_in_rule sg name rule bad_concl);
     ((name, arule), att)
   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;
 
 end;