diff -r 50b6c07c0dd4 -r 6aeb8454efc1 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Sun Nov 15 20:57:42 2009 +0100
+++ b/src/HOL/Extraction.thy	Sun Nov 15 21:58:40 2009 +0100
@@ -43,10 +43,12 @@
   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
   notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
   induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
-  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_atomize induct_rulify induct_rulify_fallback
   True_implies_equals TrueE
 
+lemmas [extraction_expand_def] =
+  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+
 datatype sumbool = Left | Right
 
 subsection {* Type of extracted program *}