--- a/src/HOL/Tools/typedef_package.ML Thu Jul 13 23:11:38 2000 +0200
+++ b/src/HOL/Tools/typedef_package.ML Thu Jul 13 23:13:10 2000 +0200
@@ -141,7 +141,7 @@
((if no_def then [] else [(name, setT, NoSyn)]) @
[(Rep_name, newT --> oldT, NoSyn),
(Abs_name, oldT --> newT, NoSyn)])
- |> (if no_def then I else (#1 oo (PureThy.add_defs_i o map Thm.no_attributes))
+ |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
[Logic.mk_defpair (setC, set)])
|> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
[(Rep_name, rep_type),