# HG changeset patch
# User haftmann
# Date 1253338527 -7200
# Node ID 210fa627d7677eea6faf28451f9d42344795e673
# Parent  2f3e7a92b52294a5d86805db3dc8e5e5c544dcc5# Parent  c477b0a62ce9dba3070ac5dc1b966a4044370068
merged

diff -r 2f3e7a92b522 -r 210fa627d767 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Sep 18 23:08:53 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Sep 19 07:35:27 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'' [] []