Moved extraction_expand declaration of listall_def outside of definition.

--- a/src/HOL/Lambda/WeakNorm.thy	Thu May 10 15:50:56 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu May 10 15:51:59 2007 +0200
@@ -20,7 +20,9 @@
 
 definition
   listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  [extraction_expand]: "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
+  "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
+
+declare listall_def [extraction_expand]
 
 theorem listall_nil: "listall P []"
   by (simp add: listall_def)