| changeset 32091 | 30e2ffbba718 |
| parent 31889 | fb2c8a687529 |
| child 32908 | 9aa8dfef16ff |
--- a/src/Tools/Code/code_printer.ML Tue Jul 21 00:56:19 2009 +0200 +++ b/src/Tools/Code/code_printer.ML Tue Jul 21 01:03:18 2009 +0200 @@ -82,7 +82,7 @@ open Code_Thingol; -fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm); +fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm); (** assembling text pieces **)