# HG changeset patch
# User wenzelm
# Date 1441023392 -7200
# Node ID 52f3256a6d85f1c090c1c6c5813f3a0b8b18d309
# Parent  0baa20dd768d8b357f2a639547e52979f0a4f540
tuned message;

diff -r 0baa20dd768d -r 52f3256a6d85 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Aug 31 05:12:14 2015 +0200
+++ b/src/Pure/context.ML	Mon Aug 31 14:16:32 2015 +0200
@@ -451,7 +451,7 @@
 
 fun certificate_theory (Certificate thy) = thy
   | certificate_theory (Certificate_Id thy_id) =
-      error ("No content for theory certificate " ^ quote (display_name thy_id));
+      error ("No content for theory certificate " ^ display_name thy_id);
 
 fun certificate_theory_id (Certificate thy) = theory_id thy
   | certificate_theory_id (Certificate_Id thy_id) = thy_id;
@@ -467,7 +467,7 @@
     else if proper_subthy_id (thy_id1, thy_id2) then cert2
     else
       error ("Cannot join unrelated theory certificates " ^
-        quote (display_name thy_id1) ^ " and " ^ quote (display_name thy_id2))
+        display_name thy_id1 ^ " and " ^ display_name thy_id2)
   end;