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