src/HOL/Tools/typedef_package.ML
changeset 6092 d9db67970c73
parent 5697 e816c4f1a396
child 6357 12448b8f92fb
equal deleted inserted replaced
6091:e3cdbd929a24 6092:d9db67970c73
   139      [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)]
   139      [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)]
   140     |> Theory.add_consts_i
   140     |> Theory.add_consts_i
   141      ((if no_def then [] else [(name, setT, NoSyn)]) @
   141      ((if no_def then [] else [(name, setT, NoSyn)]) @
   142       [(Rep_name, newT --> oldT, NoSyn),
   142       [(Rep_name, newT --> oldT, NoSyn),
   143        (Abs_name, oldT --> newT, NoSyn)])
   143        (Abs_name, oldT --> newT, NoSyn)])
   144     |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none)
   144     |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
   145      [(name ^ "_def", Logic.mk_equals (setC, set))])
   145      [(name ^ "_def", Logic.mk_equals (setC, set))])
   146     |> (PureThy.add_axioms_i o map Attribute.none)
   146     |> (PureThy.add_axioms_i o map Thm.no_attributes)
   147      [(Rep_name, rep_type),
   147      [(Rep_name, rep_type),
   148       (Rep_name ^ "_inverse", rep_type_inv),
   148       (Rep_name ^ "_inverse", rep_type_inv),
   149       (Abs_name ^ "_inverse", abs_type_inv)]
   149       (Abs_name ^ "_inverse", abs_type_inv)]
   150   end
   150   end
   151   handle ERROR =>
   151   handle ERROR =>