src/HOL/Nominal/nominal_thmdecls.ML

--- a/src/HOL/Nominal/nominal_thmdecls.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -156,7 +156,7 @@
       fold (fn thm => Data.map (flag thm)) thms_to_be_added context
   end
   handle EQVT_FORM s =>
-      error (Display.string_of_thm orig_thm ^ 
+      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
                " does not comply with the form of an equivariance lemma (" ^ s ^").")