--- a/src/HOL/Code_Evaluation.thy Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Sep 15 15:40:35 2010 +0200
@@ -315,7 +315,7 @@
fun tracing s x = (Output.tracing s; x);
-fun eval_term thy t = Code_Runtime.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
+fun eval_term thy t = Code_Runtime.value NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
I thy (HOLogic.mk_term_of (fastype_of t) t) [];
end
--- a/src/HOL/HOL.thy Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 15 15:40:35 2010 +0200
@@ -1978,7 +1978,7 @@
val t = Thm.term_of ct;
val dummy = @{cprop True};
in case try HOLogic.dest_Trueprop t
- of SOME t' => if Code_Runtime.eval NONE
+ of SOME t' => if Code_Runtime.value NONE
(Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' []
then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
else dummy
--- a/src/HOL/Library/Eval_Witness.thy Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Wed Sep 15 15:40:35 2010 +0200
@@ -59,7 +59,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if Code_Runtime.eval NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
+ if Code_Runtime.value NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end
--- 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;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 15:40:35 2010 +0200
@@ -272,7 +272,7 @@
Pos_Random_DSeq =>
let
val compiled_term =
- Code_Runtime.eval (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+ Code_Runtime.value (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
(fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
thy4 qc_term []
in
@@ -283,7 +283,7 @@
| New_Pos_Random_DSeq =>
let
val compiled_term =
- Code_Runtime.eval (SOME target)
+ Code_Runtime.value (SOME target)
(Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
@@ -297,7 +297,7 @@
end
| Depth_Limited_Random =>
let
- val compiled_term = Code_Runtime.eval (SOME target)
+ val compiled_term = Code_Runtime.value (SOME target)
(Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
(fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
g depth nrandom size seed |> (Predicate.map o map) proc)
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 15:40:35 2010 +0200
@@ -392,14 +392,14 @@
in if Quickcheck.report ctxt then
let
val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Runtime.eval (SOME target)
+ val compile = Code_Runtime.value (SOME target)
(Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
(fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
in compile #> Random_Engine.run end
else
let
val t' = mk_generator_expr thy t Ts;
- val compile = Code_Runtime.eval (SOME target)
+ val compile = Code_Runtime.value (SOME target)
(Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
(fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
val dummy_report = ([], false)