changeset 35842 | 7c170d39a808 |
parent 35806 | a814cccce0b8 |
child 35994 | 9cc3df9a606e |
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Mar 19 00:46:08 2010 +0100 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Mar 19 00:47:23 2010 +0100 @@ -82,7 +82,7 @@ *) Local_Theory.theory_result (Typedef.add_typedef_global false NONE - (qty_name, vs, mx) + (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac) lthy end