src/Tools/Code/code_target.ML

--- a/src/Tools/Code/code_target.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -97,8 +97,8 @@
       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