src/Pure/Isar/expression.ML
changeset 42359 6ca5407863ed
parent 42358 b47d41d9f4b5
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Apr 16 15:25:25 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 ctxt (ProofContext.consts_of ctxt) c), args)
     1.8 +      Term.list_comb (Syntax.free (ProofContext.extern_const ctxt c), args)
     1.9    else raise Match);
    1.10  
    1.11  (* define one predicate including its intro rule and axioms