diff -r 00f4461fa99f -r 80ef19b51493 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Apr 18 15:51:48 2016 +0100
+++ b/src/HOL/Tools/typedef.ML	Mon Apr 18 20:24:19 2016 +0200
@@ -240,8 +240,7 @@
     (* result *)
 
     fun note ((b, atts), th) =
-      Local_Theory.note ((b, map (Attrib.internal o K) atts), [th])
-      #>> (fn (_, [th']) => th');
+      Local_Theory.note ((b, atts), [th]) #>> (fn (_, [th']) => th');
 
     fun typedef_result inhabited lthy1 =
       let
@@ -260,16 +259,20 @@
           ||>> note ((Binding.suffix_name "_inject" Abs_name, []),
               make @{thm type_definition.Abs_inject})
           ||>> note ((Binding.suffix_name "_cases" Rep_name,
-                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+                [Attrib.case_names [Binding.name_of Rep_name],
+                 Attrib.internal (K (Induct.cases_pred full_name))]),
               make @{thm type_definition.Rep_cases})
           ||>> note ((Binding.suffix_name "_cases" Abs_name,
-                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]),
+                [Attrib.case_names [Binding.name_of Abs_name],
+                 Attrib.internal (K (Induct.cases_type full_name))]),
               make @{thm type_definition.Abs_cases})
           ||>> note ((Binding.suffix_name "_induct" Rep_name,
-                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+                [Attrib.case_names [Binding.name_of Rep_name],
+                 Attrib.internal (K (Induct.induct_pred full_name))]),
               make @{thm type_definition.Rep_induct})
           ||>> note ((Binding.suffix_name "_induct" Abs_name,
-                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]),
+                [Attrib.case_names [Binding.name_of Abs_name],
+                 Attrib.internal (K (Induct.induct_type full_name))]),
               make @{thm type_definition.Abs_induct});
 
         val info =