153 add_typedecls [(t, vs, mx)] |
153 add_typedecls [(t, vs, mx)] |
154 #> Theory.add_consts_i |
154 #> Theory.add_consts_i |
155 ((if def then [(name, setT', NoSyn)] else []) @ |
155 ((if def then [(name, setT', NoSyn)] else []) @ |
156 [(Rep_name, newT --> oldT, NoSyn), |
156 [(Rep_name, newT --> oldT, NoSyn), |
157 (Abs_name, oldT --> newT, NoSyn)]) |
157 (Abs_name, oldT --> newT, NoSyn)]) |
158 #> add_def (Logic.mk_defpair (setC, set)) |
158 #> add_def (PrimitiveDefs.mk_defpair (setC, set)) |
159 ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop), |
159 ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop), |
160 [apsnd (fn cond_axm => nonempty RS cond_axm)])] |
160 [apsnd (fn cond_axm => nonempty RS cond_axm)])] |
161 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
161 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
162 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
162 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
163 #-> (fn (set_def, [type_definition]) => fn thy1 => |
163 #-> (fn (set_def, [type_definition]) => fn thy1 => |