# HG changeset patch # User wenzelm # Date 1266323181 -3600 # Node ID 7b2538c987e75353c9c26a3ba95cb08511206572 # Parent 495c623f1e3cebb6ce6a3a20cd45470b0a97b2fc comment; diff -r 495c623f1e3c -r 7b2538c987e7 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Feb 16 13:06:43 2010 +0100 +++ b/src/Pure/Isar/expression.ML Tue Feb 16 13:26:21 2010 +0100 @@ -606,7 +606,7 @@ fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => if length args = n then - Syntax.const "_aprop" $ + Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) else raise Match);