217 _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c |
217 _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c |
218 | _ => error "type_introduction: bad type definition theorem" |
218 | _ => error "type_introduction: bad type definition theorem" |
219 val tfrees = Term.add_tfrees c [] |
219 val tfrees = Term.add_tfrees c [] |
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 {Rep_name = Binding.name rep_name, |
223 (SOME (Binding.name rep_name, Binding.name abs_name)) |
223 Abs_name = Binding.name abs_name, |
|
224 type_definition_name = Binding.name ("type_definition_" ^ tycname)} |
224 val ((_, typedef_info), thy') = |
225 val ((_, typedef_info), thy') = |
225 Typedef.add_typedef_global {overloaded = false} |
226 Typedef.add_typedef_global {overloaded = false} |
226 (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c |
227 (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c |
227 (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy |
228 (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy |
228 val aty = #abs_type (#1 typedef_info) |
229 val aty = #abs_type (#1 typedef_info) |