# HG changeset patch
# User krauss
# Date 1166017970 -3600
# Node ID 0fba71f35a9c00de15e6079638417ba22bd54e57
# Parent  d7bb902beb07387ce2f740ecb11985ef05611c57
simplified

diff -r d7bb902beb07 -r 0fba71f35a9c src/HOL/Tools/function_package/auto_term.ML
--- a/src/HOL/Tools/function_package/auto_term.ML	Wed Dec 13 14:52:30 2006 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Wed Dec 13 14:52:50 2006 +0100
@@ -27,12 +27,9 @@
       val Rvar = cert (Var (the_single (Term.add_vars prem [])))
     in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end
 
-fun relation_meth src =
-  Method.syntax Args.term src
-  #> (fn (ctxt, rel) => Method.SIMPLE_METHOD' (relation_tac ctxt rel))
 
 val setup = Method.add_methods
-  [("relation", relation_meth,
+  [("relation", (Method.SIMPLE_METHOD' o uncurry relation_tac) oo (Method.syntax Args.term),
     "proves termination using a user-specified wellfounded relation")]
 
 end