src/HOL/Tools/function_package/auto_term.ML
changeset 21879 a3efbae45735
parent 21815 0fba71f35a9c
child 22496 1f428200fd9c
--- a/src/HOL/Tools/function_package/auto_term.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -29,7 +29,7 @@
 
 
 val setup = Method.add_methods
-  [("relation", (Method.SIMPLE_METHOD' o uncurry relation_tac) oo (Method.syntax Args.term),
+  [("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")]
 
 end