diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Exceptions.thy
--- a/src/HOL/MicroJava/J/Exceptions.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -5,7 +5,7 @@
 
 theory Exceptions imports State begin
 
-text {* a new, blank object with default values in all fields: *}
+text \<open>a new, blank object with default values in all fields:\<close>
 definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where
   "blank G C \<equiv> (C,init_vars (fields(G,C)))"