- No longer applies norm_hhf_rule
- intrs field now contains theorems with names specified by user

--- a/src/HOL/Tools/inductive_package.ML	Wed Nov 13 15:28:41 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 13 15:31:14 2002 +0100
@@ -324,7 +324,7 @@
   end;
 
 val rulify =
-  standard o Tactic.norm_hhf_rule o
+  standard o
   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
   hol_simplify inductive_conj;
 
@@ -805,7 +805,7 @@
     {defs = fp_def :: rec_sets_defs,
      mono = mono,
      unfold = unfold,
-     intrs = intrs'',
+     intrs = intrs',
      elims = elims',
      mk_cases = mk_cases elims',
      raw_induct = rulify raw_induct,