--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sat May 17 13:54:30 2008 +0200
@@ -159,7 +159,7 @@
fold (fn thm => Data.map (flag thm)) thms_to_be_added context
end
handle EQVT_FORM s =>
- error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
+ error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
(* in cases of bij- and freshness, we just add the lemmas to the *)
(* data-slot *)