diff -r 27a04da9c6e6 -r 157e6108a342 src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Mon Apr 23 21:44:36 2012 +0200
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Tools/Function/relation.ML
     Author:     Alexander Krauss, TU Muenchen
 
-Method "relation" to start a termination proof using a user-specified relation.
+Tactics to start a termination proof using a user-specified relation.
 *)
 
 signature FUNCTION_RELATION =
 sig
   val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
-  val setup: theory -> theory
+  val relation_infer_tac: Proof.context -> term -> int -> tactic
 end
 
 structure Function_Relation : FUNCTION_RELATION =
@@ -27,7 +27,7 @@
   THEN inst_state_tac rel;
 
 
-(* method version (with type inference) *)
+(* version with type inference *)
 
 fun inst_state_infer_tac ctxt rel st =
   case Term.add_vars (prop_of st) [] of
@@ -44,12 +44,8 @@
       end
   | _ => Seq.empty;
 
-fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
+fun relation_infer_tac ctxt rel i =
   TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN inst_state_infer_tac ctxt rel);
-
-val setup =
-  Method.setup @{binding relation} (Args.term >> relation_meth)
-    "proves termination using a user-specified wellfounded relation";
+  THEN inst_state_infer_tac ctxt rel;
 
 end