comment;
authorwenzelm
Tue Feb 16 13:26:21 2010 +0100 (2010-02-16)
changeset 351437b2538c987e7
parent 35142 495c623f1e3c
child 35144 8b8302da3a55
comment;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Feb 16 13:06:43 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Feb 16 13:26:21 2010 +0100
     1.3 @@ -606,7 +606,7 @@
     1.4  
     1.5  fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
     1.6    if length args = n then
     1.7 -    Syntax.const "_aprop" $
     1.8 +    Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
     1.9        Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
    1.10    else raise Match);
    1.11