diff -r c7e1db87b98a -r c760ea8154ee src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu Sep 27 22:25:12 2001 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Thu Sep 27 22:26:00 2001 +0200
@@ -28,7 +28,7 @@
 
 (** theory context references **)
 
-val type_definitionN = "subset.type_definition";
+val type_definitionN = "Typedef.type_definition";
 val type_definition_def = thm "type_definition_def";
 
 val Rep = thm "Rep";
@@ -98,7 +98,7 @@
 
 fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy =
   let
-    val _ = Theory.requires thy "subset" "typedefs";
+    val _ = Theory.requires thy "Typedef" "typedefs";
     val sign = Theory.sign_of thy;
     val full = Sign.full_name sign;