src/Tools/nbe.ML
changeset 39911 2b4430847310
parent 39606 7af0441a3a47
child 40362 82a066bff182
     1.1 --- a/src/Tools/nbe.ML	Fri Oct 01 16:05:25 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri Oct 01 17:06:49 2010 +0200
     1.3 @@ -396,7 +396,7 @@
     1.4          s
     1.5          |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
     1.6          |> pair ""
     1.7 -        |> ML_Context.value ctxt univs_cookie
     1.8 +        |> Code_Runtime.value ctxt univs_cookie
     1.9          |> (fn f => f deps_vals)
    1.10          |> (fn univs => cs ~~ univs)
    1.11        end;