--- a/src/Pure/Isar/expression.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Isar/expression.ML Fri Apr 08 16:34:14 2011 +0200
@@ -613,7 +613,7 @@
(* 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)