src/HOL/Tools/typedef_package.ML
changeset 6092 d9db67970c73
parent 5697 e816c4f1a396
child 6357 12448b8f92fb
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Jan 12 13:40:08 1999 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Jan 12 13:54:51 1999 +0100
     1.3 @@ -141,9 +141,9 @@
     1.4       ((if no_def then [] else [(name, setT, NoSyn)]) @
     1.5        [(Rep_name, newT --> oldT, NoSyn),
     1.6         (Abs_name, oldT --> newT, NoSyn)])
     1.7 -    |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none)
     1.8 +    |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
     1.9       [(name ^ "_def", Logic.mk_equals (setC, set))])
    1.10 -    |> (PureThy.add_axioms_i o map Attribute.none)
    1.11 +    |> (PureThy.add_axioms_i o map Thm.no_attributes)
    1.12       [(Rep_name, rep_type),
    1.13        (Rep_name ^ "_inverse", rep_type_inv),
    1.14        (Abs_name ^ "_inverse", abs_type_inv)]