--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 17:34:14 2009 +0200
@@ -216,7 +216,8 @@
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.TerminationSimps.get ctxt))
+ THEN lex_order_tac ctxt
+ (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac