src/HOL/Tools/Function/relation.ML

       let val cert = Thm.cterm_of (Thm.theory_of_thm st);
       in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
   | _ => Seq.empty;
 
 fun relation_tac ctxt rel i =
-  TRY (Function_Common.apply_termination_rule ctxt i)
+  TRY (Function_Common.termination_rule_tac ctxt i)
   THEN inst_state_tac rel;
 
 
 (* version with type inference *)
 

         PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st
       end
   | _ => Seq.empty;
 
 fun relation_infer_tac ctxt rel i =
-  TRY (Function_Common.apply_termination_rule ctxt i)
+  TRY (Function_Common.termination_rule_tac ctxt i)
   THEN inst_state_infer_tac ctxt rel;
 
 end