src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML

   register_coinduct_dynamic_base fpT_name
   #> ensure_codatatype_extra fpT_name;
 
 fun is_set ctxt (const_name, T) =
   (case T of
-    Type (@{type_name fun}, [Type (fpT_name, _), Type (@{type_name set}, [_])]) =>
+    Type (\<^type_name>\<open>fun\<close>, [Type (fpT_name, _), Type (\<^type_name>\<open>set\<close>, [_])]) =>
     (case bnf_of ctxt fpT_name of
       SOME bnf => exists (fn Const (s, _) => s = const_name | _ => false) (sets_of_bnf bnf)
     | NONE => false)
   | _ => false);
 

     val fpsig_nesting_map_thms = maps #map_thms fpsig_nesting_fp_bnf_sugars;
     val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
     val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
     val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
 
-    val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = code_goal;
+    val @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal;
     val (fun_t, args) = strip_comb lhs;
     val closed_rhs = fold_rev lambda args rhs;
 
     val fun_T = fastype_of fun_t;
     val num_args = num_binder_types fun_T;

       fp_sugar_of ctxt fpT_name;
     val SOME {case_dtor, ...} = codatatype_extra_of ctxt fpT_name;
 
     val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs;
 
-    fun is_nullary_disc_def (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _
-          $ (Const (@{const_name HOL.eq}, _) $ _ $ _))) = true
-      | is_nullary_disc_def (Const (@{const_name Pure.eq}, _) $ _
-          $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
+    fun is_nullary_disc_def (@{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
+          $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true
+      | is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _
+          $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true
       | is_nullary_disc_def _ = false;
 
     val dtor_ctor = nth (#dtor_ctors fp_res) fp_res_index;
     val ctor_iff_dtor = #ctor_iff_dtor fp_ctr_sugar;
     val ctr_sugar = #ctr_sugar fp_ctr_sugar;

         $ ((algrho as Const (algrho_name, _)) $ _))) =
       Thm.prop_of cong_algrho_intro;
 
     val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
 
-    fun has_algrho (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ rhs)) =
+    fun has_algrho (@{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
       fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
 
     val eq_algrho :: _ =
       maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
 
-    val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
+    val @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
     val friend = mk_ctr fp_argTs friend0;
 
     val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
   in
     Variable.add_free_names ctxt goal []

       fp_sugar_of ctxt fpT_name;
 
     val n = length ctrXs_Tss;
     val ms = map length ctrXs_Tss;
 
-    val X' = TVar ((X_s, maxidx_of_typ fpT + 1), @{sort type});
+    val X' = TVar ((X_s, maxidx_of_typ fpT + 1), \<^sort>\<open>type\<close>);
     val As_rho = tvar_subst thy T0_args fpT_args;
     val substXAT = Term.typ_subst_TVars As_rho o Tsubst X X';
     val substXA = Term.subst_TVars As_rho o substT X X';
     val phi = Morphism.typ_morphism "BNF" substXAT $> Morphism.term_morphism "BNF" substXA;
 

 
 fun explore_nested lthy explore {bound_Us, bound_Ts, U, T} t =
   let
     fun build_simple (T, U) =
       if T = U then
-        @{term "%y. y"}
+        \<^term>\<open>%y. y\<close>
       else
         Bound 0
         |> explore {bound_Us = T :: bound_Us, bound_Ts = T :: bound_Ts, U = U, T = T}
         |> (fn t => Abs (Name.uu, T, t));
   in

     massage_any massages
   end;
 
 fun massage_let explore params t =
   (case strip_comb t of
-    (Const (@{const_name Let}, _), [_, _]) => unfold_lets_splits t
+    (Const (\<^const_name>\<open>Let\<close>, _), [_, _]) => unfold_lets_splits t
   | _ => t)
   |> explore params;
 
 fun check_corec_equation ctxt fun_frees (lhs, rhs) =
   let

         val sel_positionss = map mk_sel_positions ordered_sels;
         val sel_rhss = map2 mk_sel_rhs sel_positionss ordered_sels;
         val sel_lhss = map (rapp lhs o mk_disc_or_sel Ts) ordered_sels;
         val sel_condss = map collect_sel_condss sel_positionss;
 
-        fun is_undefined (Const (@{const_name undefined}, _)) = true
+        fun is_undefined (Const (\<^const_name>\<open>undefined\<close>, _)) = true
           | is_undefined _ = false;
       in
         sel_condss ~~ (sel_lhss ~~ sel_rhss)
         |> filter_out (is_undefined o snd o snd)
         |> map (apsnd HOLogic.mk_eq)

     val parametric_consts = Unsynchronized.ref [];
 
     (* We are assuming that set functions are marked with "[transfer_rule]" (cf. the "transfer"
        plugin). Otherwise, the "eq_algrho" tactic might fail. *)
     fun is_special_parametric_const (x as (s, _)) =
-      s = @{const_name id} orelse is_set lthy x;
+      s = \<^const_name>\<open>id\<close> orelse is_set lthy x;
 
     fun add_parametric_const s general_T T U =
       let
         fun tupleT_of_funT T =
           let val (Ts, T) = strip_type T in

           U :: [] => U
         | _ => fpT_to ssig_T default_T);
 
     fun massage_if explore_cond explore (params as {bound_Us, bound_Ts, ...}) t =
       (case strip_comb t of
-        (const as Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
+        (const as Const (\<^const_name>\<open>If\<close>, _), obj :: (branches as [_, _])) =>
         (case List.partition Term.is_dummy_pattern (map (explore params) branches) of
           (dummy_branch' :: _, []) => dummy_branch'
         | (_, [branch']) => branch'
         | (_, branches') =>
           let
             val brancheUs = map (curry fastype_of1 bound_Us) branches';
             val U = deduce_according_type (fastype_of1 (bound_Ts, hd branches)) brancheUs;
             val const_obj' = (If_const U, obj)
-              ||> explore_cond (update_UT params @{typ bool} @{typ bool})
+              ||> explore_cond (update_UT params \<^typ>\<open>bool\<close> \<^typ>\<open>bool\<close>)
               |> op $;
           in
             build_function_after_encapsulation (const $ obj) const_obj' params branches branches'
           end)
       | _ => explore params t);

           | NONE => explore params t)
       | massage_map explore params t = explore params t;
 
     fun massage_comp explore (params as {bound_Us, ...}) t =
       (case strip_comb t of
-        (Const (@{const_name comp}, _), f1 :: f2 :: args) =>
+        (Const (\<^const_name>\<open>comp\<close>, _), f1 :: f2 :: args) =>
         let
           val args' = map (typ_before explore params) args;
           val f2' = typ_before (explore_fun (map (curry fastype_of1 bound_Us) args') explore) params
             f2;
           val f1' = typ_before (explore_fun [range_type (fastype_of1 (bound_Us, f2'))] explore)

       | const_of ((sel as Const (s1, _)) :: r) (const as Const (s2, _)) =
         if s1 = s2 then SOME sel else const_of r const
       | const_of _ _ = NONE;
 
     fun massage_disc explore (params as {T, bound_Us, bound_Ts, ...}) t =
-      (case (strip_comb t, T = @{typ bool}) of
+      (case (strip_comb t, T = \<^typ>\<open>bool\<close>) of
         ((fun_t, arg :: []), true) =>
         let val arg_T = fastype_of1 (bound_Ts, arg) in
           if arg_T <> res_T then
             (case arg_T |> try (fst o dest_Type) |> Option.mapPartial (ctr_sugar_of lthy) of
               SOME {discs, T = Type (_, Ts), ...} =>

             | _ => explore params t)
           end
       end;
 
     fun massage_equality explore (params as {bound_Us, bound_Ts, ...})
-          (t as Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
+          (t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =
         let
           val check_is_VLeaf =
             not o (Term.exists_subterm (fn t => t aconv CLeaf orelse t aconv Oper));
 
           fun try_pattern_matching (fun_t, arg_ts) t =

         massage_nested_corec_call ctxt has_self_call explore' explore' bound_Ts U T t
       end;
 
     fun massage_comp explore params t =
       (case strip_comb t of
-        (Const (@{const_name comp}, _), f1 :: f2 :: args) =>
+        (Const (\<^const_name>\<open>comp\<close>, _), f1 :: f2 :: args) =>
         explore params (betapply (f1, (betapplys (f2, args))))
       | _ => explore params t);
 
     fun massage_fun explore (params as {bound_Us, bound_Ts, U, T}) t =
       if can dest_funT T then

     val ((def_fun, (_, (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))),
          lthy) =
       prepare_corec_ursive_cmd int false opts (raw_fixes, raw_eq) lthy;
   in
     if not (null termin_goals) then
-      error ("Termination prover failed (try " ^ quote (#1 @{command_keyword corecursive}) ^
-        " instead of " ^ quote (#1 @{command_keyword corec}) ^ ")")
+      error ("Termination prover failed (try " ^ quote (#1 \<^command_keyword>\<open>corecursive\<close>) ^
+        " instead of " ^ quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")")
     else if not (null const_transfer_goals) then
-      error ("Transfer prover failed (try " ^ quote (#1 @{command_keyword corecursive}) ^
-        " instead of " ^ quote (#1 @{command_keyword corec}) ^ ")")
+      error ("Transfer prover failed (try " ^ quote (#1 \<^command_keyword>\<open>corecursive\<close>) ^
+        " instead of " ^ quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")")
     else
       def_fun inner_fp_triple const_transfers [] lthy
   end;
 
 fun corecursive_cmd int opts (raw_fixes, raw_eq) lthy =

     val fun_b = Binding.name (Long_Name.base_name fun_name);
     val code_goal = Syntax.read_prop fake_lthy raw_eq;
 
     val fun_T =
       (case code_goal of
-        @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _) => fastype_of (head_of t)
+        @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
       | _ => ill_formed_equation_lhs_rhs lthy [code_goal]);
     val fun_t = Const (fun_name, fun_T);
 
     val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T;
 

 
 fun consolidate_global thy =
   SOME (Named_Target.theory_map consolidate thy)
   handle Same.SAME => NONE;
 
-val _ = Outer_Syntax.local_theory @{command_keyword corec}
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>corec\<close>
   "define nonprimitive corecursive functions"
-  ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
-      --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
+  ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 corec_option_parser)
+      --| \<^keyword>\<open>)\<close>) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
    >> uncurry (corec_cmd true));
 
-val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive}
+val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>corecursive\<close>
   "define nonprimitive corecursive functions"
-  ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
-      --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
+  ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 corec_option_parser)
+      --| \<^keyword>\<open>)\<close>) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
    >> uncurry (corecursive_cmd true));
 
-val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec}
+val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>friend_of_corec\<close>
   "register a function as a legal context for nonprimitive corecursion"
   (Parse.const -- Scan.option (Parse.$$$ "::" |-- Parse.typ) --| Parse.where_ -- Parse.prop
    >> friend_of_corec_cmd);
 
-val _ = Outer_Syntax.local_theory @{command_keyword coinduction_upto}
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>coinduction_upto\<close>
   "derive a coinduction up-to principle and a corresponding congruence closure"
   (Parse.name --| Parse.$$$ ":" -- Parse.typ >> coinduction_upto_cmd);
 
 val _ = Theory.setup (Theory.at_begin consolidate_global);