diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -167,7 +167,7 @@
 val type_equiv = Sign.typ_equiv
 
 fun varify_type ctxt T =
-  Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
+  Variable.polymorphic_types ctxt [Const (\<^const_name>\<open>undefined\<close>, T)]
   |> snd |> the_single |> dest_Const |> snd
 
 (* TODO: use "Term_Subst.instantiateT" instead? *)
@@ -202,7 +202,7 @@
         SOME k => k
       | NONE =>
         case T of
-          Type (@{type_name fun}, [T1, T2]) =>
+          Type (\<^type_name>\<open>fun\<close>, [T1, T2]) =>
           (case (aux slack avoid T1, aux slack avoid T2) of
              (k, 1) => if slack andalso k = 0 then 0 else 1
            | (0, _) => 0
@@ -210,10 +210,10 @@
            | (k1, k2) =>
              if k1 >= max orelse k2 >= max then max
              else Int.min (max, Integer.pow k2 k1))
-        | Type (@{type_name set}, [T']) => aux slack avoid (T' --> @{typ bool})
-        | @{typ prop} => 2
-        | @{typ bool} => 2 (* optimization *)
-        | @{typ nat} => 0 (* optimization *)
+        | Type (\<^type_name>\<open>set\<close>, [T']) => aux slack avoid (T' --> \<^typ>\<open>bool\<close>)
+        | \<^typ>\<open>prop\<close> => 2
+        | \<^typ>\<open>bool\<close> => 2 (* optimization *)
+        | \<^typ>\<open>nat\<close> => 0 (* optimization *)
         | Type ("Int.int", []) => 0 (* optimization *)
         | Type (s, _) =>
           (case free_constructors_of ctxt T of
@@ -260,10 +260,10 @@
 
 (* Simple simplifications to ensure that sort annotations don't leave a trail of
    spurious "True"s. *)
-fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
-    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
-  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
-    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
+fun s_not (Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', t')) =
+    Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', s_not t')
+  | s_not (Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', t')) =
+    Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', s_not t')
   | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
   | s_not (@{const HOL.conj} $ t1 $ t2) =
     @{const HOL.disj} $ s_not t1 $ s_not t2
@@ -313,7 +313,7 @@
        (Term.add_vars t []) t
 
 fun hol_open_form unprefix
-      (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
+      (t as Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, T, t')) =
     (case try unprefix s of
        SOME s =>
        let
@@ -332,15 +332,15 @@
              (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
 
 fun cong_extensionalize_term ctxt t =
-  if exists_Const (fn (s, _) => s = @{const_name Not}) t then
+  if exists_Const (fn (s, _) => s = \<^const_name>\<open>Not\<close>) t then
     t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
       |> Meson.cong_extensionalize_thm ctxt
       |> Thm.prop_of
   else
     t
 
-fun is_fun_equality (@{const_name HOL.eq},
-                     Type (_, [Type (@{type_name fun}, _), _])) = true
+fun is_fun_equality (\<^const_name>\<open>HOL.eq\<close>,
+                     Type (_, [Type (\<^type_name>\<open>fun\<close>, _), _])) = true
   | is_fun_equality _ = false
 
 fun abs_extensionalize_term ctxt t =
@@ -352,12 +352,12 @@
 
 fun unextensionalize_def t =
   case t of
-    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
+    @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) =>
     (case strip_comb lhs of
        (c as Const (_, T), args) =>
        if forall is_Var args andalso not (has_duplicates (op =) args) then
          @{const Trueprop}
-         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
+         $ (Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> \<^typ>\<open>bool\<close>)
             $ c $ fold_rev lambda args rhs)
        else
          t
@@ -370,9 +370,9 @@
    "Meson_Clausify".) *)
 fun transform_elim_prop t =
   case Logic.strip_imp_concl t of
-    @{const Trueprop} $ Var (z, @{typ bool}) =>
+    @{const Trueprop} $ Var (z, \<^typ>\<open>bool\<close>) =>
     subst_Vars [(z, @{const False})] t
-  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
+  | Var (z, \<^typ>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t
   | _ => t
 
 fun specialize_type thy (s, T) t =
@@ -401,7 +401,7 @@
     val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
   in (rev params, hyp_ts, concl_t) end
 
-fun extract_lambda_def dest_head (Const (@{const_name HOL.eq}, _) $ t $ u) =
+fun extract_lambda_def dest_head (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) =
     let val (head, args) = strip_comb t in
       (head |> dest_head |> fst,
        fold_rev (fn t as Var ((s, _), T) =>