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