1.1 --- a/src/Pure/codegen.ML	Mon Jul 25 10:40:51 2011 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Jul 25 10:40:52 2011 +0200
     1.3 @@ -916,6 +916,7 @@
     1.4  
     1.5  fun eval_term ctxt t =
     1.6    let
     1.7 +    val _ = legacy_feature "Old evaluation mechanism -- use evaluator 'code' or method eval instead";
     1.8      val thy = Proof_Context.theory_of ctxt;
     1.9      val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    1.10        error "Term to be evaluated contains type variables";