# HG changeset patch
# User wenzelm
# Date 978812787 -3600
# Node ID 306aee77eaddf4238dfdcd2d96bcb668a0814a39
# Parent  bdc3aa1c193b79593ea536f9821e2f74ba9b2a25
Tactic.norm_hhf;

diff -r bdc3aa1c193b -r 306aee77eadd src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:13 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:27 2001 +0100
@@ -266,7 +266,7 @@
   end;
 
 val rulify =
-  standard o full_simplify [Drule.norm_hhf_eq] o
+  standard o Tactic.norm_hhf o
   full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
   full_simplify inductive_conj;