changeset 58239 | 1c5bc387bd4c |
parent 58028 | e4250d370657 |
child 58959 | 1f195ed99941 |
--- a/src/HOL/Tools/Quotient/quotient_type.ML Mon Sep 08 23:04:18 2014 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Mon Sep 08 23:04:18 2014 +0200 @@ -45,7 +45,7 @@ val typedef_tac = EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in - Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx) + Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy end