diff -r 39acf19e9f3a -r 30e2ffbba718 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -39,7 +39,7 @@
 
 
 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
-  Display.string_of_thm thm);
+  Display.string_of_thm_without_context thm);
 
 fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;