--- a/src/HOL/Code_Setup.thy Mon Dec 15 09:58:44 2008 +0100
+++ b/src/HOL/Code_Setup.thy Mon Dec 15 09:58:45 2008 +0100
@@ -198,6 +198,10 @@
subsection {* Evaluation and normalization by evaluation *}
+setup {*
+ Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
+*}
+
ML {*
structure Eval_Method =
struct
@@ -240,6 +244,10 @@
subsection {* Quickcheck *}
+setup {*
+ Quickcheck.add_generator ("SML", Codegen.test_term)
+*}
+
quickcheck_params [size = 5, iterations = 50]
end
--- a/src/HOL/HOL.thy Mon Dec 15 09:58:44 2008 +0100
+++ b/src/HOL/HOL.thy Mon Dec 15 09:58:45 2008 +0100
@@ -26,6 +26,7 @@
"~~/src/Tools/atomize_elim.ML"
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
+ "~~/src/Tools/value.ML"
"~~/src/Tools/code/code_name.ML"
"~~/src/Tools/code/code_funcgr.ML"
"~~/src/Tools/code/code_thingol.ML"
--- a/src/HOL/IsaMakefile Mon Dec 15 09:58:44 2008 +0100
+++ b/src/HOL/IsaMakefile Mon Dec 15 09:58:45 2008 +0100
@@ -179,6 +179,7 @@
$(SRC)/Tools/code/code_thingol.ML \
$(SRC)/Tools/induct.ML \
$(SRC)/Tools/induct_tacs.ML \
+ $(SRC)/Tools/value.ML \
$(SRC)/Tools/nbe.ML \
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/rat.ML
--- a/src/Pure/IsaMakefile Mon Dec 15 09:58:44 2008 +0100
+++ b/src/Pure/IsaMakefile Mon Dec 15 09:58:45 2008 +0100
@@ -86,7 +86,7 @@
proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \
simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \
- variable.ML ../Tools/value.ML ../Tools/quickcheck.ML
+ variable.ML ../Tools/quickcheck.ML
@./mk
--- a/src/Pure/ROOT.ML Mon Dec 15 09:58:44 2008 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 15 09:58:45 2008 +0100
@@ -87,8 +87,6 @@
cd "Tools"; use "ROOT.ML"; cd "..";
-use "../Tools/value.ML";
-use "../Tools/quickcheck.ML";
use "codegen.ML";
(*configuration for Proof General*)
--- a/src/Pure/Tools/ROOT.ML Mon Dec 15 09:58:44 2008 +0100
+++ b/src/Pure/Tools/ROOT.ML Mon Dec 15 09:58:45 2008 +0100
@@ -11,3 +11,6 @@
(*derived theory and proof elements*)
use "invoke.ML";
+
+(*quickcheck needed here because of pg preferences*)
+use "../../Tools/quickcheck.ML"
--- a/src/Pure/codegen.ML Mon Dec 15 09:58:44 2008 +0100
+++ b/src/Pure/codegen.ML Mon Dec 15 09:58:45 2008 +0100
@@ -1025,8 +1025,6 @@
val setup = add_codegen "default" default_codegen
#> add_tycodegen "default" default_tycodegen
- #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
- #> Quickcheck.add_generator ("SML", test_term)
#> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
(fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)))
#> add_preprocessor unfold_preprocessor;