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