# HG changeset patch
# User berghofe
# Date 1170868030 -3600
# Node ID 23e0fde84cb705cc99f7870bf2ef366c0fba622f
# Parent  a20a203c8f41f29e9aeb719eb9ee3f68e582f723
Added meta_spec to extraction_expand.

diff -r a20a203c8f41 -r 23e0fde84cb7 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Wed Feb 07 18:04:44 2007 +0100
+++ b/src/HOL/Extraction.thy	Wed Feb 07 18:07:10 2007 +0100
@@ -49,7 +49,7 @@
 *}
 
 lemmas [extraction_expand] =
-  atomize_eq atomize_all atomize_imp atomize_conj
+  meta_spec atomize_eq atomize_all atomize_imp atomize_conj
   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