changeset 62969 | 9f394a16c557 |
parent 62550 | f1baa15a6a0c |
child 63024 | adeac19dd410 |
--- a/src/Tools/Code/code_target.ML Wed Apr 13 17:00:02 2016 +0200 +++ b/src/Tools/Code/code_target.ML Wed Apr 13 18:01:05 2016 +0200 @@ -104,7 +104,7 @@ fun read_inst ctxt (raw_tyco, raw_class) = (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class); -val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class; +val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class; fun cert_syms ctxt = Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))