145 [(Rep_name, newT --> oldT, NoSyn), |
145 [(Rep_name, newT --> oldT, NoSyn), |
146 (Abs_name, oldT --> newT, NoSyn)]) |
146 (Abs_name, oldT --> newT, NoSyn)]) |
147 |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes)) |
147 |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes)) |
148 [Logic.mk_defpair (setC, set)]) |
148 [Logic.mk_defpair (setC, set)]) |
149 |> PureThy.add_axioms_i [((typedef_name, typedef_prop), |
149 |> PureThy.add_axioms_i [((typedef_name, typedef_prop), |
150 [apsnd (fn cond_axm => standard (nonempty RS cond_axm))])] |
150 [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] |
151 |> (fn (theory', axm) => |
151 |> (fn (theory', axm) => |
152 let fun make th = standard (th OF axm) in |
152 let fun make th = Drule.standard (th OF axm) in |
153 rpair (hd axm) (theory' |
153 rpair (hd axm) (theory' |
154 |> (#1 oo PureThy.add_thms) |
154 |> (#1 oo PureThy.add_thms) |
155 ([((Rep_name, make Rep), []), |
155 ([((Rep_name, make Rep), []), |
156 ((Rep_name ^ "_inverse", make Rep_inverse), []), |
156 ((Rep_name ^ "_inverse", make Rep_inverse), []), |
157 ((Abs_name ^ "_inverse", make Abs_inverse), []), |
157 ((Abs_name ^ "_inverse", make Abs_inverse), []), |
191 val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; |
191 val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; |
192 val _ = if null errs then () else error (cat_lines errs); |
192 val _ = if null errs then () else error (cat_lines errs); |
193 |
193 |
194 (*test theory errors now!*) |
194 (*test theory errors now!*) |
195 val test_thy = Theory.copy thy; |
195 val test_thy = Theory.copy thy; |
196 val test_sign = Theory.sign_of test_thy; |
196 val _ = (test_thy, |
197 val _ = (test_thy, Thm.assume (Thm.cterm_of test_sign goal)) |> typedef_att; |
197 setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_att; |
198 |
198 |
199 in (cset, goal, goal_pat, typedef_att) end |
199 in (cset, goal, goal_pat, typedef_att) end |
200 handle ERROR => err_in_typedef name; |
200 handle ERROR => err_in_typedef name; |
201 |
201 |
202 |
202 |