diff -r 3daaf23b9ab4 -r 6315b6426200 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_haskell.ML
+(*  Title:      Tools/Code/code_haskell.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer for Haskell.
@@ -6,6 +6,8 @@
 
 signature CODE_HASKELL =
 sig
+  val target: string
+  val check: theory -> Path.T -> unit
   val setup: theory -> theory
 end;
 
@@ -462,6 +464,14 @@
   else error "Only Haskell target allows for monad syntax" end;
 
 
+(** formal checking of compiled code **)
+
+fun check thy = Code_Target.external_check thy target
+  "EXEC_GHC" I (fn ghc => fn p => fn module_name =>
+    ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs");
+
+
+
 (** Isar setup **)
 
 fun isar_seri_haskell module_name =