--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 22:55:00 2011 +0200
@@ -214,9 +214,10 @@
end
fun lexicographic_order_tac quiet ctxt =
- TRY (Function_Common.apply_termination_rule ctxt 1)
- THEN lex_order_tac quiet ctxt
- (auto_tac (claset_of ctxt, simpset_of ctxt addsimps Function_Common.Termination_Simps.get ctxt))
+ TRY (Function_Common.apply_termination_rule ctxt 1) THEN
+ lex_order_tac quiet ctxt
+ (auto_tac
+ (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false