1.1 --- a/src/HOL/Code_Setup.thy	Mon Dec 15 09:58:44 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Mon Dec 15 09:58:45 2008 +0100
     1.3 @@ -198,6 +198,10 @@
     1.4  
     1.5  subsection {* Evaluation and normalization by evaluation *}
     1.6  
     1.7 +setup {*
     1.8 +  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
     1.9 +*}
    1.10 +
    1.11  ML {*
    1.12  structure Eval_Method =
    1.13  struct
    1.14 @@ -240,6 +244,10 @@
    1.15  
    1.16  subsection {* Quickcheck *}
    1.17  
    1.18 +setup {*
    1.19 +  Quickcheck.add_generator ("SML", Codegen.test_term)
    1.20 +*}
    1.21 +
    1.22  quickcheck_params [size = 5, iterations = 50]
    1.23  
    1.24  end

     2.1 --- a/src/HOL/HOL.thy	Mon Dec 15 09:58:44 2008 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Dec 15 09:58:45 2008 +0100
     2.3 @@ -26,6 +26,7 @@
     2.4    "~~/src/Tools/atomize_elim.ML"
     2.5    "~~/src/Tools/induct.ML"
     2.6    ("~~/src/Tools/induct_tacs.ML")
     2.7 +  "~~/src/Tools/value.ML"
     2.8    "~~/src/Tools/code/code_name.ML"
     2.9    "~~/src/Tools/code/code_funcgr.ML"
    2.10    "~~/src/Tools/code/code_thingol.ML"

     3.1 --- a/src/HOL/IsaMakefile	Mon Dec 15 09:58:44 2008 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Mon Dec 15 09:58:45 2008 +0100
     3.3 @@ -179,6 +179,7 @@
     3.4    $(SRC)/Tools/code/code_thingol.ML \
     3.5    $(SRC)/Tools/induct.ML \
     3.6    $(SRC)/Tools/induct_tacs.ML \
     3.7 +  $(SRC)/Tools/value.ML \
     3.8    $(SRC)/Tools/nbe.ML \
     3.9    $(SRC)/Tools/random_word.ML \
    3.10    $(SRC)/Tools/rat.ML

     4.1 --- a/src/Pure/IsaMakefile	Mon Dec 15 09:58:44 2008 +0100
     4.2 +++ b/src/Pure/IsaMakefile	Mon Dec 15 09:58:45 2008 +0100
     4.3 @@ -86,7 +86,7 @@
     4.4    proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
     4.5    simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
     4.6    term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML		\
     4.7 -  variable.ML ../Tools/value.ML ../Tools/quickcheck.ML
     4.8 +  variable.ML ../Tools/quickcheck.ML
     4.9  	@./mk
    4.10  
    4.11  

     5.1 --- a/src/Pure/ROOT.ML	Mon Dec 15 09:58:44 2008 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Mon Dec 15 09:58:45 2008 +0100
     5.3 @@ -87,8 +87,6 @@
     5.4  
     5.5  cd "Tools"; use "ROOT.ML"; cd "..";
     5.6  
     5.7 -use "../Tools/value.ML";
     5.8 -use "../Tools/quickcheck.ML";
     5.9  use "codegen.ML";
    5.10  
    5.11  (*configuration for Proof General*)

     6.1 --- a/src/Pure/Tools/ROOT.ML	Mon Dec 15 09:58:44 2008 +0100
     6.2 +++ b/src/Pure/Tools/ROOT.ML	Mon Dec 15 09:58:45 2008 +0100
     6.3 @@ -11,3 +11,6 @@
     6.4  
     6.5  (*derived theory and proof elements*)
     6.6  use "invoke.ML";
     6.7 +
     6.8 +(*quickcheck needed here because of pg preferences*)
     6.9 +use "../../Tools/quickcheck.ML"

     7.1 --- a/src/Pure/codegen.ML	Mon Dec 15 09:58:44 2008 +0100
     7.2 +++ b/src/Pure/codegen.ML	Mon Dec 15 09:58:45 2008 +0100
     7.3 @@ -1025,8 +1025,6 @@
     7.4  
     7.5  val setup = add_codegen "default" default_codegen
     7.6    #> add_tycodegen "default" default_tycodegen
     7.7 -  #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
     7.8 -  #> Quickcheck.add_generator ("SML", test_term)
     7.9    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
    7.10         (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)))
    7.11    #> add_preprocessor unfold_preprocessor;