src/HOL/Nominal/nominal_inductive.ML

 
 fun mk_perm_bool ctxt pi th =
   th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
 
 fun mk_perm_bool_simproc names =
-  Simplifier.make_simproc @{context} "perm_bool"
-   {lhss = [@{term "perm pi x"}],
+  Simplifier.make_simproc \<^context> "perm_bool"
+   {lhss = [\<^term>\<open>perm pi x\<close>],
     proc = fn _ => fn _ => fn ct =>
       (case Thm.term_of ct of
-        Const (@{const_name Nominal.perm}, _) $ _ $ t =>
+        Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ t =>
           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
       | _ => NONE)};
 
 fun transp ([] :: _) = []

       | _ => fold (add_binders thy i) ts bs)
     | (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs))
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ p $ q) _ = (case head_of p of
       Const (name, _) =>
         if member (op =) names name then SOME (f p q) else NONE
     | _ => NONE)
   | split_conj _ _ _ _ = NONE;
 
 fun strip_all [] t = t
-  | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
+  | strip_all (_ :: xs) (Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, T, t)) = strip_all xs t;
 
 (*********************************************************************)
 (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
 (* or    ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)            *)
 (* to    R ... & id (ALL z. P z (pi_1 o ... o pi_n o t))             *)
 (* or    id (ALL z. P z (pi_1 o ... o pi_n o t))                     *)
 (*                                                                   *)
 (* where "id" protects the subformula from simplification            *)
 (*********************************************************************)
 
-fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ p $ q) _ =
       (case head_of p of
          Const (name, _) =>
            if member (op =) names name then SOME (HOLogic.mk_conj (p,
-             Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
+             Const (\<^const_name>\<open>Fun.id\<close>, HOLogic.boolT --> HOLogic.boolT) $
                (subst_bounds (pis, strip_all pis q))))
            else NONE
        | _ => NONE)
   | inst_conj_all names ps pis t u =
       if member (op aconv) ps (head_of u) then
-        SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
+        SOME (Const (\<^const_name>\<open>Fun.id\<close>, HOLogic.boolT --> HOLogic.boolT) $
           (subst_bounds (pis, strip_all pis t)))
       else NONE
   | inst_conj_all _ _ _ _ _ = NONE;
 
 fun inst_conj_all_tac ctxt k = EVERY

            map (apfst (incr_boundvars 1)) (mk_avoids params avoid),
          prems, strip_comb (HOLogic.dest_Trueprop concl))
       end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
 
     val atomTs = distinct op = (maps (map snd o #2) prems);
-    val ind_sort = if null atomTs then @{sort type}
+    val ind_sort = if null atomTs then \<^sort>\<open>type\<close>
       else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
         ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
     val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
     val fsT = TFree (fs_ctxt_tyname, ind_sort);

     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
       ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
     val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-      addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
+      addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
     val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
     val perm_bij = Global_Theory.get_thms thy "perm_bij";
     val fs_atoms = map (fn aT => Global_Theory.get_thm thy
       ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;

     fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
       let
         (** protect terms to avoid that fresh_prod interferes with  **)
         (** pairs used in introduction rules of inductive predicate **)
         fun protect t =
-          let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
+          let val T = fastype_of t in Const (\<^const_name>\<open>Fun.id\<close>, T --> T) $ t end;
         val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1);
         val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
             (HOLogic.exists_const T $ Abs ("x", T,
               NominalDatatype.fresh_const T (fastype_of p) $
                 Bound 0 $ p)))

                  val freshs2' = NominalDatatype.mk_not_sym freshs2;
                  val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1);
                  fun concat_perm pi1 pi2 =
                    let val T = fastype_of pi1
                    in if T = fastype_of pi2 then
-                       Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
+                       Const (\<^const_name>\<open>append\<close>, T --> T --> T) $ pi1 $ pi2
                      else pi2
                    end;
                  val pis'' = fold (concat_perm #> map) pis' pis;
                  val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
                    (Vartab.empty, Vartab.empty);

 
 
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
+  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>nominal_inductive\<close>
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
-    (Parse.name -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
-      (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
+    (Parse.name -- Scan.optional (\<^keyword>\<open>avoids\<close> |-- Parse.and_list1 (Parse.name --
+      (\<^keyword>\<open>:\<close> |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
         prove_strong_ind name avoids));
 
 val _ =
-  Outer_Syntax.local_theory @{command_keyword equivariance}
+  Outer_Syntax.local_theory \<^command_keyword>\<open>equivariance\<close>
     "prove equivariance for inductive predicate involving nominal datatypes"
-    (Parse.name -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
+    (Parse.name -- Scan.optional (\<^keyword>\<open>[\<close> |-- Parse.list1 Parse.name --| \<^keyword>\<open>]\<close>) [] >>
       (fn (name, atoms) => prove_eqvt name atoms));
 
 end