diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -1276,7 +1276,7 @@
     apply assumption
    apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
 
-  -- {* @{text "<=s"} *}
+  -- \<open>@{text "<=s"}\<close>
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
   apply (simp add: max_spec_preserves_length [symmetric])