use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges

--- a/src/HOL/HOL.thy	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 03 10:51:22 2014 +0200
@@ -2017,4 +2017,3 @@
 hide_const (open) eq equal
 
 end
-

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Apr 03 10:51:22 2014 +0200
@@ -265,7 +265,15 @@
   type T = Datatype_Aux.config * string list;
   val eq: T * T -> bool = eq_snd (op =);
 );
-fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
+
+fun with_repaired_path f config (type_names as name :: _) thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier name)
+  |> f config type_names
+  |> Sign.restore_naming thy;
+
+fun interpretation f = Datatype_Interpretation.interpretation (uncurry (with_repaired_path f));
 val interpretation_data = Datatype_Interpretation.data;
 
 

--- a/src/HOL/Tools/Function/size.ML	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Tools/Function/size.ML	Thu Apr 03 10:51:22 2014 +0200
@@ -220,8 +220,7 @@
 fun add_size_thms config (new_type_names as name :: _) thy =
   let
     val info as {descr, ...} = Datatype_Data.the_info thy name;
-    val prefix =
-      Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name;
+    val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
       Datatype_Aux.is_rec_type dt andalso
         not (null (fst (Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
@@ -229,7 +228,6 @@
     if no_size then thy
     else
       thy
-      |> Sign.root_path
       |> Sign.add_path prefix
       |> prove_size_thms info new_type_names
       |> Sign.restore_naming thy

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 03 10:51:22 2014 +0200
@@ -405,9 +405,9 @@
     val algebra = Sign.classes_of thy;
     val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
     val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
-    fun insts_of sort constr  = (map (rpair sort) o flat o maps snd o maps snd)
+    fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
       (Datatype_Aux.interpret_construction descr vs constr)
-    val insts = insts_of sort  { atyp = single, dtyp = (K o K o K) [] }
+    val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
       @ insts_of aux_sort { atyp = K [], dtyp = K o K }
     val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
   in if has_inst then thy

--- a/src/HOL/Tools/typedef.ML	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu Apr 03 10:51:22 2014 +0200
@@ -73,7 +73,15 @@
 (* global interpretation *)
 
 structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
-val interpretation = Typedef_Interpretation.interpretation;
+
+fun with_repaired_path f name thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier name)
+  |> f name
+  |> Sign.restore_naming thy;
+
+fun interpretation f = Typedef_Interpretation.interpretation (with_repaired_path f);
 
 val setup = Typedef_Interpretation.init;
 
@@ -154,8 +162,7 @@
       |> Typedecl.typedecl (name, args, mx)
       ||> Variable.declare_term set;
 
-    val Type (full_name, type_args) = newT;
-    val lhs_tfrees = map Term.dest_TFree type_args;
+    val Type (full_name, _) = newT;
 
 
     (* axiomatization *)
@@ -183,7 +190,6 @@
 
     fun typedef_result inhabited lthy1 =
       let
-        val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
         val typedef' = inhabited RS typedef;
         fun make th = Goal.norm_result lthy1 (typedef' RS th);
         val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),

--- a/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:22 2014 +0200
@@ -859,7 +859,7 @@
 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
-declare "prod.size" [no_atp]
+declare prod.size [no_atp]
 
 
 hide_const (open) acc accp

--- a/src/Pure/Isar/code.ML	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/Pure/Isar/code.ML	Thu Apr 03 10:51:22 2014 +0200
@@ -1232,8 +1232,15 @@
 structure Datatype_Interpretation =
   Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
 
+fun with_repaired_path f (tyco, serial) thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier tyco)
+  |> f (tyco, serial)
+  |> Sign.restore_naming thy;
+
 fun datatype_interpretation f = Datatype_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy);
+  (fn (tyco, _) => fn thy => with_repaired_path f (tyco, fst (get_type thy tyco)) thy);
 
 fun add_datatype proto_constrs thy =
   let