src/HOL/Tools/function_package/auto_term.ML

     val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
     val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
     val prem = #1 (Logic.dest_implies (Thm.prop_of rule'))
     val R' = cert (Var (the_single (Term.add_vars prem [])))
   in
-    resolve_tac [Drule.cterm_instantiate [(R', rel')] rule'] 1  (* produce the usual goals *)
+    rtac (Drule.cterm_instantiate [(R', rel')] rule') 1  (* instantiate termination rule *)
     THEN (ALLGOALS
       (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
         | i => asm_simp_tac ss i))             (* Simplify termination conditions *)
   end
 

     val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt)
     val ss = local_simpset_of ctxt addsimps simps
 
     val intro_rule = ProofContext.get_thm ctxt (Name "termination")
     (* FIXME avoid internal name lookup -- dynamic scoping! *)
-  in Method.RAW_METHOD (K (auto_term_tac ctxt intro_rule rel wfs ss)) end)
+  in Method.SIMPLE_METHOD (auto_term_tac ctxt intro_rule rel wfs ss) end)
 
 val setup = Method.add_methods
-  [("auto_term", termination_meth, "termination prover for recdef compatibility")]
+  [("auto_term", termination_meth, "proves termination using a user-specified wellfounded relation")]
 
 end