changeset 49835 | 31f32ec4d766 |
parent 49833 | 1d80798e8d8a |
child 50177 | 2006c50172c9 |
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 18:58:20 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 21:22:35 2012 +0200 @@ -45,7 +45,7 @@ val typedef_tac = EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in - Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx) + Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy end