# HG changeset patch
# User wenzelm
# Date 981148809 -3600
# Node ID 3c30f7b97a50708b2ced32bb9604dd649cccabff
# Parent  bad7568e76e0fc4399466b2bf36c9f30f8eb0cde
use hol_simplify;

diff -r bad7568e76e0 -r 3c30f7b97a50 src/HOL/Tools/inductive_package.ML
--- 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;