diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 18:44:09 2009 +0200
@@ -217,7 +217,7 @@
 fun lexicographic_order_tac ctxt =
   TRY (FundefCommon.apply_termination_rule ctxt 1)
   THEN lex_order_tac ctxt
-    (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
+    (auto_tac (clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
 
 val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac