src/HOL/Tools/Function/lexicographic_order.ML

           THEN EVERY (map prove_row clean_table))
         end
   end) 1 st;
 
 fun lexicographic_order_tac quiet ctxt =
-  TRY (Function_Common.apply_termination_rule ctxt 1) THEN
+  TRY (Function_Common.termination_rule_tac ctxt 1) THEN
   lex_order_tac quiet ctxt
     (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp})))
 
 val _ =
   Theory.setup