diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stefan Berghofer
 *)
 
-section {* Example for generating executable code from Java semantics *}
+section \<open>Example for generating executable code from Java semantics\<close>
 
 theory JListExample
 imports Eval
@@ -151,7 +151,7 @@
   "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
 by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
 
-ML_val {* 
+ML_val \<open>
   val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
   locs @{code l1_name};
   locs @{code l2_name};
@@ -177,6 +177,6 @@
 
   val_field (Suc (Suc (Suc @{code "0 :: nat"})));
   next_field (Suc (Suc (Suc @{code "0 :: nat"})));
-*}
+\<close>
 
 end