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