| changeset 32091 | 30e2ffbba718 |
| parent 31998 | 2c7a24f74db9 |
| child 32287 | 65d5c5b30747 |
--- 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;