--- a/src/Pure/Isar/expression.ML Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/expression.ML Sat Apr 16 13:48:45 2011 +0200
@@ -616,7 +616,7 @@
fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
if length args = n then
Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *)
- Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
+ Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args)
else raise Match);
(* define one predicate including its intro rule and axioms