src/HOL/Tools/inductive_package.ML
changeset 10804 306aee77eadd
parent 10743 8ea821d1e3a4
child 10910 058775a575db
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:13 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:27 2001 +0100
     1.3 @@ -266,7 +266,7 @@
     1.4    end;
     1.5  
     1.6  val rulify =
     1.7 -  standard o full_simplify [Drule.norm_hhf_eq] o
     1.8 +  standard o Tactic.norm_hhf o
     1.9    full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
    1.10    full_simplify inductive_conj;
    1.11