220 | _ => error "type_introduction: bad type definition theorem" |
220 | _ => error "type_introduction: bad type definition theorem" |
221 val tfrees = Term.add_tfrees c [] |
221 val tfrees = Term.add_tfrees c [] |
222 val tnames = sort_strings (map fst tfrees) |
222 val tnames = sort_strings (map fst tfrees) |
223 val ((_, typedef_info), thy') = |
223 val ((_, typedef_info), thy') = |
224 Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c |
224 Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c |
225 (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy |
225 (SOME (Binding.name rep_name, Binding.name abs_name)) (fn _ => rtac th2 1) thy |
226 val aty = #abs_type (#1 typedef_info) |
226 val aty = #abs_type (#1 typedef_info) |
227 val th = freezeT (#type_definition (#2 typedef_info)) |
227 val th = freezeT (#type_definition (#2 typedef_info)) |
228 val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th)) |
228 val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th)) |
229 val (th_s, abst) = Thm.dest_comb th_s |
229 val (th_s, abst) = Thm.dest_comb th_s |
230 val rept = Thm.dest_arg th_s |
230 val rept = Thm.dest_arg th_s |