src/HOL/Extraction.thy

--- a/src/HOL/Extraction.thy	Tue Nov 13 10:59:26 2007 +0100
+++ b/src/HOL/Extraction.thy	Tue Nov 13 11:00:29 2007 +0100
@@ -55,7 +55,7 @@
   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
+  True_implies_equals TrueE
 
 datatype sumbool = Left | Right