author | wenzelm |
Sun, 03 Jan 2010 15:08:17 +0100 | |
changeset 34236 | 010a3206cbbe |
parent 34235 | 43bf58fdbace |
child 34237 | 225daff4323b |
--- a/src/HOL/Tools/Function/termination.ML Sun Jan 03 11:03:22 2010 +0000 +++ b/src/HOL/Tools/Function/termination.ML Sun Jan 03 15:08:17 2010 +0100 @@ -412,8 +412,8 @@ cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i end) -val derive_diag = gen_descent true -val derive_all = gen_descent false +fun derive_diag ctxt = gen_descent true ctxt +fun derive_all ctxt = gen_descent false ctxt end