--- a/src/Tools/Code/code_printer.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/Tools/Code/code_printer.ML Sat Feb 01 18:42:46 2014 +0100
@@ -11,7 +11,7 @@
type const = Code_Thingol.const
type dict = Code_Thingol.dict
- val eqn_error: thm option -> string -> 'a
+ val eqn_error: theory -> thm option -> string -> 'a
val @@ : 'a * 'a -> 'a list
val @| : 'a list * 'a -> 'a list
@@ -100,9 +100,9 @@
(** generic nonsense *)
-fun eqn_error (SOME thm) s =
- error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
- | eqn_error NONE s = error s;
+fun eqn_error thy (SOME thm) s =
+ error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
+ | eqn_error _ NONE s = error s;
val code_presentationN = "code_presentation";
val stmt_nameN = "stmt_name";