src/HOL/Tools/typedef_package.ML
changeset 9315 f793f05024f6
parent 9230 17ae63f82ad8
child 9969 4753185f1dd2
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Jul 13 23:11:38 2000 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Jul 13 23:13:10 2000 +0200
     1.3 @@ -141,7 +141,7 @@
     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 (#1 oo (PureThy.add_defs_i o map Thm.no_attributes))
     1.8 +      |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
     1.9         [Logic.mk_defpair (setC, set)])
    1.10        |> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
    1.11         [(Rep_name, rep_type),