# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 479a779b89a69581512a92ded79de58c137bf97e
# Parent  81f7e60755c331f4ef15416e6275a2c0dcdf2ffd
use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture

diff -r 81f7e60755c3 -r 479a779b89a6 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -62,7 +62,7 @@
     val new_type_names = map (Binding.name_of o fst) types_syntax;
     val big_name = space_implode "_" new_type_names;
     val thy1 = Sign.add_path big_name thy;
-    val big_rec_name = big_name ^ "_rep_set";
+    val big_rec_name = "rep_set_" ^ big_name;
     val rep_set_names' =
       if length descr' = 1 then [big_rec_name]
       else map (prefix (big_rec_name ^ "_") o string_of_int) (1 upto length descr');
diff -r 81f7e60755c3 -r 479a779b89a6 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -87,7 +87,7 @@
 
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
-    val big_rec_name' = big_name ^ "_rec_set";
+    val big_rec_name' = "rec_set_" ^ big_name;
     val rec_set_names' =
       if length descr' = 1 then [big_rec_name']
       else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto length descr');
@@ -215,7 +215,7 @@
 
     (* define primrec combinators *)
 
-    val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
+    val big_reccomb_name = "rec_" ^ space_implode "_" new_type_names;
     val reccomb_names =
       map (Sign.full_bname thy1)
         (if length descr' = 1 then [big_reccomb_name]
@@ -289,7 +289,7 @@
           val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
         in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
 
-    val case_names0 = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
+    val case_names0 = map (fn s => Sign.full_bname thy1 ("case_" ^ s)) new_type_names;
 
     (* define case combinators via primrec combinators *)