--- 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;