# 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);