# HG changeset patch
# User wenzelm
# Date 973879637 -3600
# Node ID be2dc95dfe98afbbeffa93128d05c93299311362
# Parent  6c3901071d67d9096a3dda3f14b88dd3ad3dbcd9
inductive_rulify2 accomodates malformed induction rules;

diff -r 6c3901071d67 -r be2dc95dfe98 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Fri Nov 10 19:06:54 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Fri Nov 10 19:07:17 2000 +0100
@@ -21,7 +21,8 @@
 (** theory context references **)
 
 val inductive_atomize = thms "inductive_atomize";
-val inductive_rulify = thms "inductive_rulify";
+val inductive_rulify1 = thms "inductive_rulify1";
+val inductive_rulify2 = thms "inductive_rulify2";
 
 
 
@@ -194,9 +195,13 @@
   in Thm.cterm_of sign (drop t) handle TERM _ => ct end;
 
 val atomize_cterm = drop_Trueprop o rewrite_cterm inductive_atomize;
-val atomize_tac = Method.rewrite_goal_tac inductive_atomize;
-val rulify_cterm = rewrite_cterm inductive_rulify;
-val rulify_tac = Method.rewrite_goal_tac inductive_rulify;
+val atomize_tac = Tactic.rewrite_goal_tac inductive_atomize;
+val rulify_cterm = rewrite_cterm inductive_rulify2 o rewrite_cterm inductive_rulify1;
+
+val rulify_tac =
+  Tactic.rewrite_goal_tac inductive_rulify1 THEN'
+  Tactic.rewrite_goal_tac inductive_rulify2 THEN'
+  Proof.norm_hhf_tac;
 
 fun rulify_cases cert =
   map (apsnd (apsnd (map (Thm.term_of o rulify_cterm o cert)))) ooo RuleCases.make;