# HG changeset patch
# User haftmann
# Date 1179567201 -7200
# Node ID 00c0e4c42396e325d5b9af20724d59cc1a833591
# Parent  fd7cd1edc18df4347773443946cf257018a74fba
uniform module names for code generation

diff -r fd7cd1edc18d -r 00c0e4c42396 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat May 19 11:33:20 2007 +0200
+++ b/src/HOL/Divides.thy	Sat May 19 11:33:21 2007 +0200
@@ -929,10 +929,13 @@
   by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
 
 code_modulename SML
-  Divides Integer
+  Divides Nat
 
 code_modulename OCaml
-  Divides Integer
+  Divides Nat
+
+code_modulename Haskell
+  Divides Nat
 
 hide (open) const divmod dvd_nat
 
diff -r fd7cd1edc18d -r 00c0e4c42396 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Sat May 19 11:33:20 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Sat May 19 11:33:21 2007 +0200
@@ -388,6 +388,10 @@
   Nat Integer
   EfficientNat Integer
 
+code_modulename Haskell
+  Nat Integer
+  EfficientNat Integer
+
 hide const nat_of_int
 
 end
diff -r fd7cd1edc18d -r 00c0e4c42396 src/HOL/Library/Executable_Real.thy
--- a/src/HOL/Library/Executable_Real.thy	Sat May 19 11:33:20 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy	Sat May 19 11:33:21 2007 +0200
@@ -467,6 +467,18 @@
   "number_of k = real_int (number_of k)"
   by (simp add: real_int_def)
 
+code_modulename SML
+  RealDef Real
+  Executable_Real Real
+
+code_modulename OCaml
+  RealDef Real
+  Executable_Real Real
+
+code_modulename Haskell
+  RealDef Real
+  Executable_Real Real
+
 types_code real ("{* int * int *}")
 attach (term_of) {*
 fun term_of_real (p, q) =