src/HOL/HOLCF/Tools/cont_proc.ML

 val cont_A = @{thm cont2cont_APP}
 val cont_L = @{thm cont2cont_LAM}
 val cont_R = @{thm cont_Rep_cfun2}
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
+fun is_lcf_term (Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
+  | is_lcf_term (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ Abs (_, _, t)) =
       is_lcf_term t
-  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
+  | is_lcf_term (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ t) =
       is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = not (Term.is_open t)
 
 (*

     in (map (fn y => SOME (k y RS Lx)) ys, x') end
 
   (* first list: cont thm for each dangling bound variable *)
   (* second list: cont thm for each LAM in t *)
   (* if b = false, only return cont thm for outermost LAMs *)
-  fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
+  fun cont_thms1 b (Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ t) =
     let
       val (cs1,ls1) = cont_thms1 b f
       val (cs2,ls2) = cont_thms1 b t
     in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
-    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
+    | cont_thms1 b (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ Abs (_, _, t)) =
     let
       val (cs, ls) = cont_thms1 b t
       val (cs', l) = lam cs
     in (cs', l::ls) end
-    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
+    | cont_thms1 b (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ t) =
     let
       val t' = Term.incr_boundvars 1 t $ Bound 0
       val (cs, ls) = cont_thms1 b t'
       val (cs', l) = lam cs
     in (cs', l::ls) end

     fun new_cont_tac f' i =
       case all_cont_thms f' of
         [] => no_tac
       | (c::_) => resolve_tac ctxt [c] i
 
-    fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
+    fun cont_tac_of_term (Const (\<^const_name>\<open>cont\<close>, _) $ f) =
       let
-        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f
+        val f' = Const (\<^const_name>\<open>Abs_cfun\<close>, dummyT) $ f
       in
         if is_lcf_term f'
         then new_cont_tac f'
         else REPEAT_ALL_NEW (resolve_tac ctxt rules)
       end

       val t = Thm.term_of ct
       val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
 in
   val cont_proc =
-    Simplifier.make_simproc @{context} "cont_proc"
-     {lhss = [@{term "cont f"}], proc = K solve_cont}
+    Simplifier.make_simproc \<^context> "cont_proc"
+     {lhss = [\<^term>\<open>cont f\<close>], proc = K solve_cont}
 end
 
 val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc])
 
 end