# HG changeset patch
# User paulson
# Date 1103204063 -3600
# Node ID db69af736ebbd2feb386bc5c780b6db2ced0f55f
# Parent  6e437e276ef5c22989f1a5af4ae93ef8a3c66496
Further fix to a bug (involving equational premises) in inductive definitions

diff -r 6e437e276ef5 -r db69af736ebb src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Dec 16 12:44:32 2004 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 16 14:34:23 2004 +0100
@@ -675,7 +675,7 @@
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
-         ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
+         ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
          EVERY (map (fn prem =>
    	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);