src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML

     is_finite           : bool,
     take_induct_thms    : thm list
   }
 
 val beta_ss =
-  simpset_of (put_simpset HOL_basic_ss @{context}
-    addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}])
+  simpset_of (put_simpset HOL_basic_ss \<^context>
+    addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
 
 (******************************************************************************)
 (******************************** theory data *********************************)
 (******************************************************************************)
 

 
 fun add_rec_type (tname, bs) =
     Rec_Data.map (Symtab.insert (K true) (tname, bs))
 
 fun add_deflation_thm thm =
-    Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm)
+    Context.theory_map (Named_Theorems.add_thm \<^named_theorems>\<open>domain_deflation\<close> thm)
 
 val get_rec_tab = Rec_Data.get
 fun get_deflation_thms thy =
-  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation})
-
-val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
+  rev (Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\<open>domain_deflation\<close>)
+
+val map_ID_add = Named_Theorems.add \<^named_theorems>\<open>domain_map_ID\<close>
 fun get_map_ID_thms thy =
-  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID})
+  rev (Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\<open>domain_map_ID\<close>)
 
 
 (******************************************************************************)
 (************************** building types and terms **************************)
 (******************************************************************************)

 infixr 6 ->>
 infix -->>
 infix 9 `
 
 fun mk_deflation t =
-  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
+  Const (\<^const_name>\<open>deflation\<close>, Term.fastype_of t --> boolT) $ t
 
 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
 
 (******************************************************************************)
 (****************************** isomorphism info ******************************)

       fold_map prove_chain_take (take_consts ~~ dbinds) thy
 
     (* prove take_0 lemmas *)
     fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy =
       let
-        val lhs = take_const $ @{term "0::nat"}
+        val lhs = take_const $ \<^term>\<open>0::nat\<close>
         val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
         val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}
         fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
         val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context)
       in

     val n = Free ("n", natT)
     val take_is = map (fn t => t $ n) take_consts
     fun prove_take_Suc
           (((take_const, rep_abs), dbind), (_, rhsT)) thy =
       let
-        val lhs = take_const $ (@{term Suc} $ n)
+        val lhs = take_const $ (\<^term>\<open>Suc\<close> $ n)
         val body = map_of_typ thy (newTs ~~ take_is) rhsT
         val rhs = mk_cfcomp2 (rep_abs, body)
         val goal = mk_eqs (lhs, rhs)
         val simps = @{thms iterate_Suc fst_conv snd_conv}
         val rules = take_defs @ simps

         fun iso_locale (info : iso_info) =
             @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info]
         val iso_locale_thms = map iso_locale iso_infos
         val decisive_abs_rep_thms =
             map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms
-        val n = Free ("n", @{typ nat})
+        val n = Free ("n", \<^typ>\<open>nat\<close>)
         fun mk_decisive t =
-            Const (@{const_name decisive}, fastype_of t --> boolT) $ t
+            Const (\<^const_name>\<open>decisive\<close>, fastype_of t --> boolT) $ t
         fun f take_const = mk_decisive (take_const $ n)
         val goal = mk_trp (foldr1 mk_conj (map f take_consts))
         val rules0 = @{thm decisive_bottom} :: take_0_thms
         val rules1 =
             take_Suc_thms @ decisive_abs_rep_thms

       fold_map prove_reach_lemma
         (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy
 
     (* test for finiteness of domain definitions *)
     local
-      val types = [@{type_name ssum}, @{type_name sprod}]
+      val types = [\<^type_name>\<open>ssum\<close>, \<^type_name>\<open>sprod\<close>]
       fun finite d T = if member (op =) absTs T then d else finite' d T
       and finite' d (Type (c, Ts)) =
           let val d' = d andalso member (op =) types c
           in forall (finite d') Ts end
         | finite' _ _ = true