# HG changeset patch
# User haftmann
# Date 1334856984 -7200
# Node ID 1ba213363d0c24eaf261426e3fcf316ffb2741bc
# Parent  d6a3b69f4404a6ff0864b51ec7db43568e648bf5
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator

diff -r d6a3b69f4404 -r 1ba213363d0c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Apr 21 15:26:05 2012 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 19 19:36:24 2012 +0200
@@ -7,16 +7,19 @@
 theory HOL
 imports Pure "~~/src/Tools/Code_Generator"
 keywords
-  "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag
+  "try" "solve_direct" "quickcheck"
+    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
+  "quickcheck_params" :: thy_decl
 uses
   ("Tools/hologic.ML")
+  "~~/src/Tools/misc_legacy.ML"
+  "~~/src/Tools/try.ML"
+  "~~/src/Tools/quickcheck.ML"
+  "~~/src/Tools/solve_direct.ML"
   "~~/src/Tools/IsaPlanner/zipper.ML"
   "~~/src/Tools/IsaPlanner/isand.ML"
   "~~/src/Tools/IsaPlanner/rw_tools.ML"
   "~~/src/Tools/IsaPlanner/rw_inst.ML"
-  "~~/src/Tools/intuitionistic.ML"
-  "~~/src/Tools/project_rule.ML"
-  "~~/src/Tools/cong_tac.ML"
   "~~/src/Provers/hypsubst.ML"
   "~~/src/Provers/splitter.ML"
   "~~/src/Provers/classical.ML"
@@ -28,6 +31,9 @@
   ("Tools/simpdata.ML")
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
+  "~~/src/Tools/cong_tac.ML"
+  "~~/src/Tools/intuitionistic.ML"
+  "~~/src/Tools/project_rule.ML"
   ("~~/src/Tools/induction.ML")
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/cnf_funcs.ML")
@@ -35,10 +41,13 @@
   "~~/src/Tools/case_product.ML"
 begin
 
-setup {* Intuitionistic.method_setup @{binding iprover} *}
-setup Subtyping.setup
-setup Case_Product.setup
-
+setup {*
+  Intuitionistic.method_setup @{binding iprover}
+  #> Quickcheck.setup
+  #> Solve_Direct.setup
+  #> Subtyping.setup
+  #> Case_Product.setup
+*}
 
 subsection {* Primitive logic *}
 
@@ -2008,3 +2017,4 @@
 hide_const (open) eq equal
 
 end
+
diff -r d6a3b69f4404 -r 1ba213363d0c src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Sat Apr 21 15:26:05 2012 +0200
+++ b/src/Tools/Code_Generator.thy	Thu Apr 19 19:36:24 2012 +0200
@@ -7,19 +7,14 @@
 theory Code_Generator
 imports Pure
 keywords
-  "try" "solve_direct" "quickcheck" "value" "print_codeproc"
-    "code_thms" "code_deps" "export_code" :: diag and
-  "quickcheck_params" "code_class" "code_instance" "code_type"
+  "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
+  "code_class" "code_instance" "code_type"
     "code_const" "code_reserved" "code_include" "code_modulename"
     "code_abort" "code_monad" "code_reflect" :: thy_decl and
   "datatypes" "functions" "module_name" "file" "checking"
 uses
-  "~~/src/Tools/misc_legacy.ML"
+  "~~/src/Tools/value.ML"
   "~~/src/Tools/cache_io.ML"
-  "~~/src/Tools/try.ML"
-  "~~/src/Tools/solve_direct.ML"
-  "~~/src/Tools/quickcheck.ML"
-  "~~/src/Tools/value.ML"
   "~~/src/Tools/Code/code_preproc.ML"
   "~~/src/Tools/Code/code_thingol.ML"
   "~~/src/Tools/Code/code_simp.ML"
@@ -34,15 +29,13 @@
 begin
 
 setup {*
-  Solve_Direct.setup
+  Value.setup
   #> Code_Preproc.setup
   #> Code_Simp.setup
   #> Code_Target.setup
   #> Code_ML.setup
   #> Code_Haskell.setup
   #> Code_Scala.setup
-  #> Quickcheck.setup
-  #> Value.setup
 *}
 
 code_datatype "TYPE('a\<Colon>{})"
@@ -80,3 +73,4 @@
 hide_const (open) holds
 
 end
+