changeset 49833 | 1d80798e8d8a |
parent 47983 | a5e699834f2d |
child 49835 | 31f32ec4d766 |
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 15:08:29 2012 +0200 @@ -45,7 +45,7 @@ val typedef_tac = EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in - Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx) + Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy end