220 val tnames = sort_strings (map fst tfrees) |
220 val tnames = sort_strings (map fst tfrees) |
221 val typedef_bindings = |
221 val typedef_bindings = |
222 Typedef.make_morphisms (Binding.name tycname) |
222 Typedef.make_morphisms (Binding.name tycname) |
223 (SOME (Binding.name rep_name, Binding.name abs_name)) |
223 (SOME (Binding.name rep_name, Binding.name abs_name)) |
224 val ((_, typedef_info), thy') = |
224 val ((_, typedef_info), thy') = |
225 Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c |
225 Typedef.add_typedef_global {overloaded = false} |
|
226 (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c |
226 (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy |
227 (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy |
227 val aty = #abs_type (#1 typedef_info) |
228 val aty = #abs_type (#1 typedef_info) |
228 val th = freezeT thy' (#type_definition (#2 typedef_info)) |
229 val th = freezeT thy' (#type_definition (#2 typedef_info)) |
229 val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) |
230 val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) |
230 val (th_s, abst) = Thm.dest_comb th_s |
231 val (th_s, abst) = Thm.dest_comb th_s |