# HG changeset patch # User bulwahn # Date 1311583252 -7200 # Node ID 4611af362cd03c8101c01039ab8c9e3c9f010e88 # Parent efc6f0a81c364427dd134ad2771551ba1196b681 added legacy warning to old code generation evaluation diff -r efc6f0a81c36 -r 4611af362cd0 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";