merged

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 21 14:25:38 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 21 16:21:12 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 14:25:38 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Oct 21 16:21:12 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)

--- a/src/Pure/Isar/method.ML	Fri Oct 21 14:25:38 2011 +0200
+++ b/src/Pure/Isar/method.ML	Fri Oct 21 16:21:12 2011 +0200
@@ -366,7 +366,7 @@
       end;
   in meth end;
 
-fun method thy = method_i thy o Args.map_name (Name_Space.intern (#1 (Methods.get thy)));
+fun method thy = method_i thy o Args.map_name (intern thy);
 
 
 (* method setup *)