diff -r e9ab4ad7bd15 -r 23307fd33906 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -10,15 +10,15 @@
 "fun_rep [] = (\<lambda>x. \<top>)" |
 "fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
 
-lemma fun_rep_map_of[code]: --"original def is too slow"
+lemma fun_rep_map_of[code]: \<comment>"original def is too slow"
   "fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
 by(induction ps rule: fun_rep.induct) auto
 
 definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
-hide_type st  --"hide previous def to avoid long names"
-declare [[typedef_overloaded]] --"allow quotient types to depend on classes"
+hide_type st  \<comment>"hide previous def to avoid long names"
+declare [[typedef_overloaded]] \<comment>"allow quotient types to depend on classes"
 
 quotient_type 'a st = "('a::top) st_rep" / eq_st
 morphisms rep_st St