changeset 56002 | 2028467b4df4 |
parent 55951 | c07d184aebe9 |
child 56201 | dd2df97b379b |
--- a/src/Tools/Code/code_target.ML Sun Mar 09 15:21:08 2014 +0100 +++ b/src/Tools/Code/code_target.ML Sun Mar 09 16:37:56 2014 +0100 @@ -98,7 +98,7 @@ in tyco end; fun read_tyco ctxt = - #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true}; + #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt; fun cert_class ctxt class = let