avoid "Code" as structure name (cf. 3bc39cfe27fe)
--- 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];
--- 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]
--- 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)
--- 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 *)