theorem names generated by the (rep_)datatype command now have mandatory qualifiers

--- a/src/HOL/Product_Type.thy	Fri Dec 03 10:03:10 2010 +0100
+++ b/src/HOL/Product_Type.thy	Fri Dec 03 10:03:13 2010 +0100
@@ -160,7 +160,7 @@
 
 declare prod.simps(2) [nitpick_simp del]
 
-declare weak_case_cong [cong del]
+declare prod.weak_case_cong [cong del]
 
 
 subsubsection {* Tuple syntax *}
@@ -440,7 +440,7 @@
 
 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   -- {* Prevents simplification of @{term c}: much faster *}
-  by (fact weak_case_cong)
+  by (fact prod.weak_case_cong)
 
 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   by (simp add: split_eta)
@@ -578,7 +578,7 @@
   \medskip @{term split} used as a logical connective or set former.
 
   \medskip These rules are for use with @{text blast}; could instead
-  call @{text simp} using @{thm [source] split} as rewrite. *}
+  call @{text simp} using @{thm [source] prod.split} as rewrite. *}
 
 lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
   apply (simp only: split_tupled_all)

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 10:03:10 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 10:03:13 2010 +0100
@@ -628,9 +628,9 @@
 
     val ([dt_induct'], thy7) =
       thy6
-      |> Sign.add_path big_name
-      |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
-      ||> Sign.parent_path
+      |> Global_Theory.add_thms
+        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
+          [case_names_induct])]
       ||> Theory.checkpoint;
 
   in

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 03 10:03:10 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 03 10:03:13 2010 +0100
@@ -98,18 +98,18 @@
 
 fun store_thmss_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
-    Sign.add_path tname
-    #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
-    #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+    Global_Theory.add_thmss
+      [((Binding.qualify true tname (Binding.name label), thms), atts)]
+    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
 
 fun store_thms_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
-    Sign.add_path tname
-    #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
-    #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+    Global_Theory.add_thms
+      [((Binding.qualify true tname (Binding.name label), thms), atts)]
+    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 03 10:03:10 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 03 10:03:13 2010 +0100
@@ -362,14 +362,14 @@
   let
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+    val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val (((inject, distinct), [induct]), thy2) =
       thy1
       |> store_thmss "inject" new_type_names raw_inject
       ||>> store_thmss "distinct" new_type_names raw_distinct
-      ||> Sign.add_path (space_implode "_" new_type_names)
       ||>> Global_Theory.add_thms
-        [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
-      ||> Sign.restore_naming thy1;
+        [((prfx (Binding.name "induct"), raw_induct),
+          [mk_case_names_induct descr])];
   in
     thy2
     |> derive_datatype_props config dt_names alt_names [descr] sorts