# HG changeset patch
# User haftmann
# Date 1179988661 -7200
# Node ID a3f11e0ae90fcea742a3983fed8ce728bd7b3cb1
# Parent  ad7244663431d205feccd7b6c2631b5bde33e01c
tuned warning

diff -r ad7244663431 -r a3f11e0ae90f src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Thu May 24 08:37:39 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Thu May 24 08:37:41 2007 +0200
@@ -32,7 +32,7 @@
 fun bad_thm msg = raise BAD_THM msg;
 fun error_thm f thm = f thm handle BAD_THM msg => error msg;
 fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
-  => (warning msg; NONE);
+  => (warning ("code generator: " ^ msg); NONE);
 
 
 (* making rewrite theorems *)