# HG changeset patch
# User haftmann
# Date 1174077138 -3600
# Node ID b4f96f343d6cd0786dfb58a51d4fb87b5412fa17
# Parent  8469640e1489af070f0f4e95a81cc16e17a48f99
inf_fun_eq and inf_bool_eq now with meta equality

diff -r 8469640e1489 -r b4f96f343d6c src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Mar 16 21:32:15 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 16 21:32:18 2007 +0100
@@ -533,7 +533,7 @@
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
          REPEAT (resolve_tac [le_funI, le_boolI] 1),
-         rewrite_goals_tac (map mk_meta_eq [inf_fun_eq, inf_bool_eq] @ simp_thms'),
+         rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: 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