src/HOL/Tools/typedef_package.ML
changeset 11608 c760ea8154ee
parent 11426 f280d4b29a2c
child 11727 a27150cc8fa5
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Sep 27 22:25:12 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Sep 27 22:26:00 2001 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  (** theory context references **)
     1.6  
     1.7 -val type_definitionN = "subset.type_definition";
     1.8 +val type_definitionN = "Typedef.type_definition";
     1.9  val type_definition_def = thm "type_definition_def";
    1.10  
    1.11  val Rep = thm "Rep";
    1.12 @@ -98,7 +98,7 @@
    1.13  
    1.14  fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy =
    1.15    let
    1.16 -    val _ = Theory.requires thy "subset" "typedefs";
    1.17 +    val _ = Theory.requires thy "Typedef" "typedefs";
    1.18      val sign = Theory.sign_of thy;
    1.19      val full = Sign.full_name sign;
    1.20