src/Pure/Isar/expression.ML
changeset 42290 b1f544c84040
parent 41585 45d7da4e4ccf
child 42357 3305f573294e
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Apr 08 15:48:14 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Apr 08 16:34:14 2011 +0200
     1.3 @@ -613,7 +613,7 @@
     1.4  
     1.5  (* achieve plain syntax for locale predicates (without "PROP") *)
     1.6  
     1.7 -fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args =>
     1.8 +fun aprop_tr' n c = (Lexicon.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)