src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

       (case lookup_pred (Envir.eta_contract t) of
         SOME pred => [(pred, (names, prems))]
       | NONE =>
           let
             val (vars, body) = strip_abs t
-            val _ = @{assert} (fastype_of body = body_type (fastype_of body))
+            val _ = \<^assert> (fastype_of body = body_type (fastype_of body))
             val absnames = Name.variant_list names (map fst vars)
             val frees = map2 (curry Free) absnames (map snd vars)
             val body' = subst_bounds (rev frees, body)
             val resname = singleton (Name.variant_list (absnames @ names)) "res"
             val resvar = Free (resname, fastype_of body)

       | flatten' (t as _ $ _) (names, prems) =
       if is_constrt ctxt t orelse keep_functions thy t then
         [(t, (names, prems))]
       else
         case (fst (strip_comb t)) of
-          Const (@{const_name "If"}, _) =>
+          Const (\<^const_name>\<open>If\<close>, _) =>
             (let
               val (_, [B, x, y]) = strip_comb t
             in
               flatten' B (names, prems)
               |> maps (fn (B', (names, prems)) =>

                 @ (flatten' y (names, prems)
                 |> map (fn (res, (names, prems)) =>
                   (* in general unsound! *)
                   (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems)))))
             end)
-        | Const (@{const_name "Let"}, _) =>
+        | Const (\<^const_name>\<open>Let\<close>, _) =>
             (let
               val (_, [f, g]) = strip_comb t
             in
               flatten' f (names, prems)
               |> maps (fn (res, (names, prems)) =>

           end
       | NONE =>
           let
             val (f, args) = strip_comb t
             val args = map (Envir.eta_long []) args
-            val _ = @{assert} (fastype_of t = body_type (fastype_of t))
+            val _ = \<^assert> (fastype_of t = body_type (fastype_of t))
             val f' = lookup_pred f
             val Ts =
               (case f' of
                 SOME pred => (fst (split_last (binder_types (fastype_of pred))))
               | NONE => binder_types (fastype_of f))

                   let
                     fun lift_arg T t =
                       if (fastype_of t) = T then t
                       else
                         let
-                          val _ = @{assert} (T =
-                            (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
+                          val _ = \<^assert> (T =
+                            (binder_types (fastype_of t) @ [\<^typ>\<open>bool\<close>] ---> \<^typ>\<open>bool\<close>))
                           fun mk_if T (b, t, e) =
-                            Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
+                            Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T --> T --> T) $ b $ t $ e
                           val Ts = binder_types (fastype_of t)
                         in
-                          fold_rev Term.abs (map (pair "x") Ts @ [("b", @{typ bool})])
-                            (mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
-                              HOLogic.mk_eq (@{term True}, Bound 0),
-                              HOLogic.mk_eq (@{term False}, Bound 0)))
+                          fold_rev Term.abs (map (pair "x") Ts @ [("b", \<^typ>\<open>bool\<close>)])
+                            (mk_if \<^typ>\<open>bool\<close> (list_comb (t, map Bound (length Ts downto 1)),
+                              HOLogic.mk_eq (\<^term>\<open>True\<close>, Bound 0),
+                              HOLogic.mk_eq (\<^term>\<open>False\<close>, Bound 0)))
                         end
                     val argvs' = map2 lift_arg Ts argvs
                     val resname = singleton (Name.variant_list names') "res"
                     val resvar = Free (resname, body_type (fastype_of t))
                     val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))

 fun pred_of thy f =
   let
     val (name, T) = dest_Const f
     val base_name' = (Long_Name.base_name name ^ "P")
     val name' = Sign.full_bname thy base_name'
-    val T' = if (body_type T = @{typ bool}) then T else pred_type T
+    val T' = if (body_type T = \<^typ>\<open>bool\<close>) then T else pred_type T
   in
     (name', Const (name', T'))
   end
 
 (* assumption: mutual recursive predicates all have the same parameters. *)

         ((dst_funs ~~ dst_preds) @ lifted_args)
           (Fun_Pred.get thy)
       fun lookup_pred t = lookup thy net t
       (* create intro rules *)
       fun mk_intros ((func, pred), (args, rhs)) =
-        if (body_type (fastype_of func) = @{typ bool}) then
+        if (body_type (fastype_of func) = \<^typ>\<open>bool\<close>) then
          (* TODO: preprocess predicate definition of rhs *)
           [Logic.list_implies
             ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
         else
           let