diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Apr 28 11:52:04 2010 +0200
@@ -225,6 +225,6 @@
   Method.setup @{binding lexicographic_order}
     (Method.sections clasimp_modifiers >> (K lexicographic_order))
     "termination prover for lexicographic orderings"
-  #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
+  #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
 
 end;