# HG changeset patch
# User bulwahn
# Date 1315320022 -7200
# Node ID f523923d81824dfe03a2d3d038f0a50d34b39749
# Parent  bdf8eb8f126b1a13df6e58f7f8d0b12764e98036
avoid "Code" as structure name (cf. 3bc39cfe27fe)

diff -r bdf8eb8f126b -r f523923d8182 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 14:25:16 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 16:40:22 2011 +0200
@@ -4,7 +4,7 @@
 import Control.Exception;
 import System.IO;
 import System.Exit;
-import Code;
+import Generated_Code;
 
 type Pos = [Int];
 
diff -r bdf8eb8f126b -r f523923d8182 src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 14:25:16 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 16:40:22 2011 +0200
@@ -8,7 +8,7 @@
 import System.Exit
 import Maybe
 import List (partition, findIndex)
-import Code
+import Generated_Code
 
 
 type Pos = [Int]
diff -r bdf8eb8f126b -r f523923d8182 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 14:25:16 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 16:40:22 2011 +0200
@@ -235,17 +235,17 @@
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     fun run in_path = 
       let
-        val code_file = Path.append in_path (Path.basic "Code.hs")
+        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
         val main_file = Path.append in_path (Path.basic "Main.hs")
         val main = "module Main where {\n\n" ^
           "import System;\n" ^
           "import Narrowing_Engine;\n" ^
-          "import Code;\n\n" ^
-          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
+          "import Generated_Code;\n\n" ^
+          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
           "}\n"
-        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
-          (unprefix "module Code where {" code)
+        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
+          (unprefix "module Generated_Code where {" code)
         val _ = File.write code_file code'
         val _ = File.write narrowing_engine_file
           (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
diff -r bdf8eb8f126b -r f523923d8182 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Sep 06 14:25:16 2011 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Sep 06 16:40:22 2011 +0200
@@ -394,7 +394,7 @@
 
 fun check_code_for thy target strict args naming program names_cs =
   let
-    val module_name = "Code";
+    val module_name = "Generated_Code";
     val { env_var, make_destination, make_command } =
       (#check o the_fundamental thy) target;
     fun ext_check p =
@@ -435,7 +435,7 @@
 fun evaluator thy target naming program consts =
   let
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target NONE "Code" [] naming program consts;
+      target NONE "Generated_Code" [] naming program consts;
   in evaluation mounted_serializer prepared_program consts end;
 
 end; (* local *)