--- a/src/HOL/Tools/inductive_package.ML Fri Feb 02 22:19:52 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Feb 02 22:20:09 2001 +0100
@@ -292,8 +292,7 @@
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
@@ -321,8 +320,8 @@
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;