src/HOL/Tools/Quotient/quotient_type.ML

       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
       (Parse_Spec.overloaded -- (Parse.type_args -- Parse.binding --
         Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
           Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
-        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
+        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.thm))
       >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
 
 end