# HG changeset patch
# User wenzelm
# Date 1262527697 -3600
# Node ID 010a3206cbbe294eed0bcb977dd817d7b9262d0a
# Parent  43bf58fdbacea7affe8622d6878e7cd67e4db320
made SML/NJ happy;

diff -r 43bf58fdbace -r 010a3206cbbe src/HOL/Tools/Function/termination.ML
--- 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