--- 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;