src/Pure/Isar/expression.ML
changeset 42358 b47d41d9f4b5
parent 42357 3305f573294e
child 42359 6ca5407863ed
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Apr 16 12:46:18 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Apr 16 13:48:45 2011 +0200
     1.3 @@ -616,7 +616,7 @@
     1.4  fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
     1.5    if length args = n then
     1.6      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
     1.7 -      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
     1.8 +      Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args)
     1.9    else raise Match);
    1.10  
    1.11  (* define one predicate including its intro rule and axioms