diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/decompose.ML
--- a/src/HOL/Tools/Function/decompose.ML	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML	Thu Jul 23 18:44:09 2009 +0200
@@ -98,7 +98,7 @@
 
 fun auto_decompose_tac ctxt =
     Termination.TERMINATION ctxt
-      (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
+      (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
                      (K (K all_tac)) (K (K no_tac)))