src/Pure/Isar/expression.ML
changeset 35143 7b2538c987e7
parent 35021 c839a4c670c6
child 35204 214ec053128e
     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