src/HOL/List.thy

--- a/src/HOL/List.thy	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/List.thy	Wed Aug 25 18:36:22 2010 +0200
@@ -732,7 +732,7 @@
 in
 
 val list_eq_simproc =
-  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
 
 end;