changeset 36521 | 73ed9f18fdd3 |
parent 36519 | 46bf776a81e0 |
child 36523 | a294e4ebe0a3 |
--- a/src/HOL/Tools/Function/fun.ML Wed Apr 28 10:31:15 2010 +0200 +++ b/src/HOL/Tools/Function/fun.ML Wed Apr 28 11:52:04 2010 +0200 @@ -153,7 +153,7 @@ |> add fixes statements config |> by_pat_completeness_auto int |> Local_Theory.restore - |> termination_by (Function_Common.get_termination_prover lthy) int + |> termination_by (SIMPLE_METHOD o Function_Common.get_termination_prover lthy) int val add_fun = gen_fun Function.function val add_fun_cmd = gen_fun Function.function_cmd