src/HOL/Tools/inductive_package.ML

       | _ => err_in_rule sg name rule bad_concl);
     ((name, arule), att)
   end;
 
 val rulify =
-  standard o Tactic.norm_hhf_rule o
+  standard o
   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
   hol_simplify inductive_conj;
 
 end;
 

       |>> Theory.parent_path;
   in (thy3,
     {defs = fp_def :: rec_sets_defs,
      mono = mono,
      unfold = unfold,
-     intrs = intrs'',
+     intrs = intrs',
      elims = elims',
      mk_cases = mk_cases elims',
      raw_induct = rulify raw_induct,
      induct = induct'})
   end;