src/HOL/Nominal/nominal_thmdecls.ML

       | _ => raise EQVT_FORM "Type unknown")
   in
       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 *)
 
 fun eqvt_map f (r:Data.T)  = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r};