src/HOL/Tools/function_package/auto_term.ML

     in 
       Drule.cterm_instantiate [(Rvar, rel')] st' 
     end
 
 fun relation_tac ctxt rel i = 
-    FundefCommon.apply_termination_rule ctxt i 
+    TRY (FundefCommon.apply_termination_rule ctxt i)
     THEN PRIMITIVE (inst_thm ctxt rel)
 
 val setup = Method.add_methods
   [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
     "proves termination using a user-specified wellfounded relation")]