Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned message;
authorwenzelm
Mon, 31 Aug 2015 14:16:32 +0200
changeset 61062 52f3256a6d85
parent 61061 0baa20dd768d
child 61063 d0c21a68d9c6
tuned message;
src/Pure/context.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle