src/Tools/Code/code_target.ML

   let
     val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
       else error ("No such type constructor: " ^ quote tyco);
   in tyco end;
 
-fun read_tyco ctxt = #1 o dest_Type
-  o Proof_Context.read_type_name_proper ctxt true;
+fun read_tyco ctxt =
+  #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
 
 fun cert_class ctxt class =
   let
     val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
   in class end;