src/HOL/Tools/inductive_package.ML

   error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
     "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
 
 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
 
-val atomize_cterm = InductMethod.rewrite_cterm inductive_atomize;
-fun full_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
+val atomize_cterm = hol_rewrite_cterm inductive_atomize;
 
 in
 
 fun check_rule sg cs ((name, rule), att) =
   let

     ((name, arule), att)
   end;
 
 val rulify =
   standard o Tactic.norm_hhf o
-  full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
-  full_simplify inductive_conj;
+  hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
+  hol_simplify inductive_conj;
 
 end;