# HG changeset patch
# User haftmann
# Date 1253282456 -7200
# Node ID c477b0a62ce9dba3070ac5dc1b966a4044370068
# Parent  c0056c2c1d17dff5c2231537ca51d25399e8f168
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs

diff -r c0056c2c1d17 -r c477b0a62ce9 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Sep 18 14:40:24 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Sep 18 16:00:56 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'' [] []