diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/IMPP/Com.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
     Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
 *)
 
-section {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
+section \<open>Semantics of arithmetic and boolean expressions, Syntax of commands\<close>
 
 theory Com
 imports Main
@@ -83,10 +83,10 @@
   "WT_bodies = (!(pn,b):set bodies. WT b)"
 
 
-ML {*
+ML \<open>
   fun make_imp_tac ctxt =
     EVERY' [resolve_tac ctxt [mp], fn i => assume_tac ctxt (i + 1), eresolve_tac ctxt [thin_rl]]
-*}
+\<close>
 
 lemma finite_dom_body: "finite (dom body)"
 apply (unfold body_def)