107 (case opt_morphs of |
107 (case opt_morphs of |
108 NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name) |
108 NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name) |
109 | SOME morphs => morphs) |
109 | SOME morphs => morphs) |
110 |
110 |
111 val ((abs_t, (_, abs_def)), lthy2) = lthy1 |
111 val ((abs_t, (_, abs_def)), lthy2) = lthy1 |
112 |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm)) |
112 |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm)) |
113 val ((rep_t, (_, rep_def)), lthy3) = lthy2 |
113 val ((rep_t, (_, rep_def)), lthy3) = lthy2 |
114 |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm)) |
114 |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm)) |
115 |
115 |
116 (* quot_type theorem *) |
116 (* quot_type theorem *) |
117 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 |
117 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 |
118 |
118 |
119 (* quotient theorem *) |
119 (* quotient theorem *) |