# HG changeset patch
# User haftmann
# Date 1229331525 -3600
# Node ID 8f38bf68d42e1923d3b97a297bd9f716ee286359
# Parent  a5ac0bc68e2bbe98e989c16fbe1147b0b13b1389
moved value.ML to src/Tools

diff -r a5ac0bc68e2b -r 8f38bf68d42e src/HOL/Code_Setup.thy
--- 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
diff -r a5ac0bc68e2b -r 8f38bf68d42e src/HOL/HOL.thy
--- 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"
diff -r a5ac0bc68e2b -r 8f38bf68d42e src/HOL/IsaMakefile
--- 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
diff -r a5ac0bc68e2b -r 8f38bf68d42e src/Pure/IsaMakefile
--- 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
 
 
diff -r a5ac0bc68e2b -r 8f38bf68d42e src/Pure/ROOT.ML
--- 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*)
diff -r a5ac0bc68e2b -r 8f38bf68d42e src/Pure/Tools/ROOT.ML
--- 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"
diff -r a5ac0bc68e2b -r 8f38bf68d42e src/Pure/codegen.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;