--- a/src/HOL/Tools/function_package/lexicographic_order.ML Wed Dec 05 14:32:17 2007 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Wed Dec 05 14:36:58 2007 +0100
@@ -323,8 +323,9 @@
THEN EVERY (map prove_row clean_table))
end
-fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1
- THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
+fun lexicographic_order thms ctxt =
+ Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1)
+ THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
"termination prover for lexicographic orderings")]