src/HOL/Tools/datatype_package.ML
changeset 16486 1a12cdb6ee6b
parent 16430 bc07926e4f03
child 16646 666774b0d1b0
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jun 20 22:13:58 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 20 22:13:59 2005 +0200
     1.3 @@ -339,7 +339,7 @@
     1.4                                   val eq_ct = cterm_of sg eq_t;
     1.5                                   val Datatype_thy = theory "Datatype";
     1.6                                   val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
     1.7 -                                   map (get_thm Datatype_thy o rpair NONE)
     1.8 +                                   map (get_thm Datatype_thy o Name)
     1.9                                       ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
    1.10                               in (case (#distinct (datatype_info_err sg tname1)) of
    1.11                                   QuickAndDirty => SOME (Thm.invoke_oracle
    1.12 @@ -644,7 +644,7 @@
    1.13        Theory.parent_path |>>>
    1.14        add_and_get_axiomss "inject" new_type_names
    1.15          (DatatypeProp.make_injs descr sorts);
    1.16 -    val size_thms = if no_size then [] else get_thms thy3 ("size", NONE);
    1.17 +    val size_thms = if no_size then [] else get_thms thy3 (Name "size");
    1.18      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
    1.19        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
    1.20