src/Pure/Isar/expression.ML
changeset 35262 9ea4445d2ccf
parent 35238 18ae6ef02fe0
child 35624 c4e29a0bb8c1
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Feb 21 21:41:29 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Feb 21 22:35:02 2010 +0100
     1.3 @@ -604,7 +604,7 @@
     1.4  
     1.5  (* achieve plain syntax for locale predicates (without "PROP") *)
     1.6  
     1.7 -fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
     1.8 +fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args =>
     1.9    if length args = n then
    1.10      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
    1.11        Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)