# HG changeset patch
# User berghofe
# Date 1037197874 -3600
# Node ID ec00ba43aee82d2f72f26cd9074935fd34bbcae7
# Parent  a3a410782c9550b0ccee0eb32ca755227eb8c977
- No longer applies norm_hhf_rule
- intrs field now contains theorems with names specified by user

diff -r a3a410782c95 -r ec00ba43aee8 src/HOL/Tools/inductive_package.ML
--- 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,