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