made SML/NJ happy;
authorwenzelm
Sun Jan 03 15:08:17 2010 +0100 (2010-01-03)
changeset 34236010a3206cbbe
parent 34235 43bf58fdbace
child 34237 225daff4323b
made SML/NJ happy;
src/HOL/Tools/Function/termination.ML
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Sun Jan 03 11:03:22 2010 +0000
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Sun Jan 03 15:08:17 2010 +0100
     1.3 @@ -412,8 +412,8 @@
     1.4      cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
     1.5    end)
     1.6  
     1.7 -val derive_diag = gen_descent true
     1.8 -val derive_all = gen_descent false
     1.9 +fun derive_diag ctxt = gen_descent true ctxt
    1.10 +fun derive_all ctxt = gen_descent false ctxt
    1.11  
    1.12  
    1.13  end