2139 ML {*DatatypePackage.get_datatype @{theory} "List.list"*}

  2139 ML {*Datatype.get_datatype @{theory} "List.list"*}