src/Pure/Isar/expression.ML

     else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
   end;
 
 (* achieve plain syntax for locale predicates (without "PROP") *)
 
-fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args =>
+fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
   if length args = n then
     Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
       Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   else raise Match);