diff -r cf7f3465eaf1 -r 240563fbf41d src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/CCL/Term.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-section {* Definitions of usual program constructs in CCL *}
+section \<open>Definitions of usual program constructs in CCL\<close>
 
 theory Term
 imports CCL
@@ -52,7 +52,7 @@
   "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)"
                         [0,0,0,0,0,60] 60)
 
-ML {*
+ML \<open>
 (** Quantifier translations: variable binding **)
 
 (* FIXME does not handle "_idtdummy" *)
@@ -91,21 +91,21 @@
          val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
      in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
       end;
-*}
+\<close>
 
-parse_translation {*
+parse_translation \<open>
  [(@{syntax_const "_let"}, K let_tr),
   (@{syntax_const "_letrec"}, K letrec_tr),
   (@{syntax_const "_letrec2"}, K letrec2_tr),
   (@{syntax_const "_letrec3"}, K letrec3_tr)]
-*}
+\<close>
 
-print_translation {*
+print_translation \<open>
  [(@{const_syntax let}, K let_tr'),
   (@{const_syntax letrec}, K letrec_tr'),
   (@{const_syntax letrec2}, K letrec2_tr'),
   (@{const_syntax letrec3}, K letrec3_tr')]
-*}
+\<close>
 
 consts
   napply     :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
@@ -156,7 +156,7 @@
   and genrec_defs = letrec_def letrec2_def letrec3_def
 
 
-subsection {* Beta Rules, including strictness *}
+subsection \<open>Beta Rules, including strictness\<close>
 
 lemma letB: "\<not> t=bot \<Longrightarrow> let x be t in f(x) = f(t)"
   apply (unfold let_def)
@@ -200,11 +200,11 @@
 
 lemmas rawBs = caseBs applyB applyBbot
 
-method_setup beta_rl = {*
+method_setup beta_rl = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (CHANGED o
       simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB}))))
-*}
+\<close>
 
 lemma ifBtrue: "if true then t else u = t"
   and ifBfalse: "if false then t else u = u"
@@ -272,7 +272,7 @@
   napplyBzero napplyBsucc
 
 
-subsection {* Constructors are injective *}
+subsection \<open>Constructors are injective\<close>
 
 lemma term_injs:
   "(inl(a) = inl(a')) \<longleftrightarrow> (a=a')"
@@ -282,16 +282,16 @@
   by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
 
 
-subsection {* Constructors are distinct *}
+subsection \<open>Constructors are distinct\<close>
 
-ML {*
+ML \<open>
 ML_Thms.bind_thms ("term_dstncts",
   mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
     [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
-*}
+\<close>
 
 
-subsection {* Rules for pre-order @{text "[="} *}
+subsection \<open>Rules for pre-order @{text "[="}\<close>
 
 lemma term_porews:
   "inl(a) [= inl(a') \<longleftrightarrow> a [= a'"
@@ -301,11 +301,11 @@
   by (simp_all add: data_defs ccl_porews)
 
 
-subsection {* Rewriting and Proving *}
+subsection \<open>Rewriting and Proving\<close>
 
-ML {*
+ML \<open>
   ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
-*}
+\<close>
 
 lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews