diff -r 24d70f4e690d -r aad9f3cfa1d9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 15:40:35 2010 +0200
@@ -3277,7 +3277,7 @@
             val [nrandom, size, depth] = arguments
           in
             rpair NONE (fst (DSequence.yieldn k
-              (Code_Runtime.eval NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
+              (Code_Runtime.value NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
                 (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   thy t' [] nrandom size
                 |> Random_Engine.run)
@@ -3285,7 +3285,7 @@
           end
       | DSeq =>
           rpair NONE (fst (DSequence.yieldn k
-            (Code_Runtime.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
+            (Code_Runtime.value NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
               DSequence.map thy t' []) (the_single arguments) true))
       | New_Pos_Random_DSeq =>
           let
@@ -3295,14 +3295,14 @@
             if stats then
               apsnd (SOME o accumulate) (split_list
               (fst (Lazy_Sequence.yieldn k
-                (Code_Runtime.eval NONE
+                (Code_Runtime.value NONE
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa (apfst proc))
                     thy t' [] nrandom size seed depth))))
             else rpair NONE
               (fst (Lazy_Sequence.yieldn k
-                (Code_Runtime.eval NONE
+                (Code_Runtime.value NONE
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa proc)
@@ -3310,7 +3310,7 @@
           end
       | _ =>
           rpair NONE (fst (Predicate.yieldn k
-            (Code_Runtime.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
+            (Code_Runtime.value NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
               Predicate.map thy t' [])))
   in ((T, ts), statistics) end;