# HG changeset patch
# User berghofe
# Date 1190968553 -7200
# Node ID 6ded9235c2b67cac25c69ca289f59213648d53ff
# Parent  6d42be359d575d4b33a06fc6b8146b562440931a
prove_strong_ind now uses InductivePackage.rulify.

diff -r 6d42be359d57 -r 6ded9235c2b6 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Sep 28 10:32:38 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Sep 28 10:35:53 2007 +0200
@@ -19,11 +19,6 @@
 val inductive_forall_def = thm "induct_forall_def";
 val inductive_atomize = thms "induct_atomize";
 val inductive_rulify = thms "induct_rulify";
-val inductive_rulify_fallback = thms "induct_rulify_fallback";
-
-val rulify =
-  hol_simplify inductive_rulify
-  #> hol_simplify inductive_rulify_fallback;
 
 fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
 
@@ -412,7 +407,7 @@
         val ind_case_names = RuleCases.case_names induct_cases;
         val strong_raw_induct =
           mk_proof thy (map (map atomize_intr) thss) |>
-          rulify |> MetaSimplifier.norm_hhf;
+          InductivePackage.rulify;
         val strong_induct =
           if length names > 1 then
             (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])