src/HOL/Tools/Datatype/datatype_data.ML

 
 
 (** document antiquotation **)
 
 val antiq_setup =
-  Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
+  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = false, strict = true})
     (fn {source = src, context = ctxt, ...} => fn dtco =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val (vs, cos) = the_spec thy dtco;
         val ty = Type (dtco, map TFree vs);