added legacy warning to old code generation evaluation
authorbulwahn
Mon, 25 Jul 2011 10:40:52 +0200
changeset 43956 4611af362cd0
parent 43955 efc6f0a81c36
child 43957 64f88ef1835e
added legacy warning to old code generation evaluation
src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Jul 25 10:40:51 2011 +0200
+++ b/src/Pure/codegen.ML	Mon Jul 25 10:40:52 2011 +0200
@@ -916,6 +916,7 @@
 
 fun eval_term ctxt t =
   let
+    val _ = legacy_feature "Old evaluation mechanism -- use evaluator 'code' or method eval instead";
     val thy = Proof_Context.theory_of ctxt;
     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
       error "Term to be evaluated contains type variables";