# HG changeset patch
# User bulwahn
# Date 1299836258 -3600
# Node ID 383bbdad1650779f8717c9c1fd68b13cecd8cc84
# Parent  3bd9a21366d2ee547057c8a5e41fc5dd3a141f0c
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype

diff -r 3bd9a21366d2 -r 383bbdad1650 src/HOL/Library/LSC.thy
--- a/src/HOL/Library/LSC.thy	Fri Mar 11 10:37:37 2011 +0100
+++ b/src/HOL/Library/LSC.thy	Fri Mar 11 10:37:38 2011 +0100
@@ -9,6 +9,16 @@
 
 subsection {* Counterexample generator *}
 
+subsubsection {* Code generation setup *}
+
+code_type typerep
+  ("Haskell" "Typerep")
+
+code_const Typerep.Typerep
+  ("Haskell" "Typerep")
+
+code_reserved Haskell Typerep
+
 subsubsection {* Type code_int for Haskell's Int type *}
 
 typedef (open) code_int = "UNIV \<Colon> int set"
diff -r 3bd9a21366d2 -r 383bbdad1650 src/HOL/Tools/LSC/lazysmallcheck.ML
--- a/src/HOL/Tools/LSC/lazysmallcheck.ML	Fri Mar 11 10:37:37 2011 +0100
+++ b/src/HOL/Tools/LSC/lazysmallcheck.ML	Fri Mar 11 10:37:38 2011 +0100
@@ -25,7 +25,7 @@
 
 fun value ctxt (get, put, put_ml) (code, value) =
   let
-    val prefix = "LSC"
+    val tmp_prefix = "LSC"
     fun make_cmd executable files =
       getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^
         " -o " ^ executable ^ " && " ^ executable
@@ -39,7 +39,9 @@
           "import Code;\n\n" ^
           "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^
           "}\n"
-        val _ = File.write code_file code
+        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
+          (unprefix "module Code where {" code)
+        val _ = File.write code_file code'
         val _ = File.write lsc_file lsc_module
         val _ = File.write main_file main
         val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
@@ -47,7 +49,7 @@
       in
         bash_output cmd
       end 
-    val result = Isabelle_System.with_tmp_dir prefix run
+    val result = Isabelle_System.with_tmp_dir tmp_prefix run
     val output_value = the_default "NONE"
       (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
     val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml