# HG changeset patch
# User nipkow
# Date 1253348374 -7200
# Node ID 0bc4f7e3e2d3e32f165058084569666e034b9559
# Parent  210fa627d7677eea6faf28451f9d42344795e673# Parent  76dddd260d2f3d1bd0d34760f78460ff9bb02d11
merged

diff -r 76dddd260d2f -r 0bc4f7e3e2d3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Sep 19 10:19:12 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Sep 19 10:19:34 2009 +0200
@@ -103,6 +103,7 @@
       "(P & True) = P" "(True & P) = P"
     by (fact simp_thms)+};
 
+val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
 
 
 (** context data **)
@@ -559,7 +560,7 @@
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
          REPEAT (resolve_tac [le_funI, le_boolI] 1),
-         rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'),
+         rewrite_goals_tac simp_thms'',
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
@@ -568,7 +569,7 @@
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
-             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
+             (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
            conjI, refl] 1)) prems)]);
 
     val lemma = SkipProof.prove ctxt'' [] []