tuned;

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 21 11:26:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 21 11:27:21 2011 +0200
@@ -201,8 +201,8 @@
 
     (*********************** definition of constructors ***********************)
 
-    val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_";
-    val rep_names = map (curry op ^ "Rep_") new_type_names;
+    val big_rep_name = space_implode "_" new_type_names ^ "_Rep_";
+    val rep_names = map (prefix "Rep_") new_type_names;
     val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
       (1 upto (length (flat (tl descr))));
     val all_rep_names = map (Sign.intern_const thy3) rep_names @

--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Oct 21 11:26:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Oct 21 11:27:21 2011 +0200
@@ -217,7 +217,7 @@
     val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
 
-    val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
+    val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
     val reccomb_names = map (Sign.intern_const thy)
       (if length descr' = 1 then [big_reccomb_name] else
         (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)