use hol_simplify;
authorwenzelm
Fri Feb 02 22:20:09 2001 +0100 (2001-02-02 ago)
changeset 110363c30f7b97a50
parent 11035 bad7568e76e0
child 11037 37716a82a3d9
use hol_simplify;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Feb 02 22:19:52 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Feb 02 22:20:09 2001 +0100
     1.3 @@ -292,8 +292,7 @@
     1.4  
     1.5  val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
     1.6  
     1.7 -val atomize_cterm = InductMethod.rewrite_cterm inductive_atomize;
     1.8 -fun full_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
     1.9 +val atomize_cterm = hol_rewrite_cterm inductive_atomize;
    1.10  
    1.11  in
    1.12  
    1.13 @@ -321,8 +320,8 @@
    1.14  
    1.15  val rulify =
    1.16    standard o Tactic.norm_hhf o
    1.17 -  full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
    1.18 -  full_simplify inductive_conj;
    1.19 +  hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
    1.20 +  hol_simplify inductive_conj;
    1.21  
    1.22  end;
    1.23