src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML

   else
     let
       val binding = mk_binding config type_name
       val final_fqn = Sign.full_name thy binding
       val tyargs =
-        List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int)
+        List.tabulate (arity, rpair \<^sort>\<open>type\<close> o prefix "'" o string_of_int)
       val (_, thy') =
         Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy
       val typ_map_entry = (thf_type, (final_fqn, arity))
       val ty_map' = typ_map_entry :: ty_map
     in (ty_map', thy') end

   | fmlatype_to_type (Fmla (Interpreted_ExtraLogic Apply, [tm1, tm2])) =
       (case fmlatype_to_type tm1 of
         Atom_type (str, tys) => Atom_type (str, tys @ [fmlatype_to_type tm2]))
 
 fun tfree_name_of_var_type str = "'" ^ Name.desymbolize (SOME false) str
-fun tfree_of_var_type str = TFree (tfree_name_of_var_type str, @{sort type})
+fun tfree_of_var_type str = TFree (tfree_name_of_var_type str, \<^sort>\<open>type\<close>)
 
 fun interpret_type config thy type_map thf_ty =
   let
     fun lookup_type ty_map ary str =
       (case AList.lookup (op =) ty_map str of

               raise MISINTERPRET_SYMBOL ("TPTP type used with wrong arity",
                 Uninterpreted str))
   in
     case thf_ty of
        Prod_type (thf_ty1, thf_ty2) =>
-         Type (@{type_name prod},
+         Type (\<^type_name>\<open>prod\<close>,
           [interpret_type config thy type_map thf_ty1,
            interpret_type config thy type_map thf_ty2])
      | Fn_type (thf_ty1, thf_ty2) =>
-         Type (@{type_name fun},
+         Type (\<^type_name>\<open>fun\<close>,
           [interpret_type config thy type_map thf_ty1,
            interpret_type config thy type_map thf_ty2])
      | Atom_type (str, thf_tys) =>
          Type (lookup_type type_map (length thf_tys) str,
            map (interpret_type config thy type_map) thf_tys)
      | Var_type str => tfree_of_var_type str
      | Defined_type tptp_base_type =>
          (case tptp_base_type of
-            Type_Ind => @{typ ind}
+            Type_Ind => \<^typ>\<open>ind\<close>
           | Type_Bool => HOLogic.boolT
           | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
           (*FIXME these types are currently unsupported, so they're treated as
           individuals*)
           (*

            |> (Term.absdummy dummyT #> Term.absdummy dummyT)
         | Or => HOLogic.disj
         | And => HOLogic.conj
         | Iff => HOLogic.eq_const HOLogic.boolT
         | If => HOLogic.imp
-        | Fi => @{term "\<lambda> x. \<lambda> y. y \<longrightarrow> x"}
+        | Fi => \<^term>\<open>\<lambda> x. \<lambda> y. y \<longrightarrow> x\<close>
         | Xor =>
-            @{term
-              "\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)"}
-        | Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}
-        | Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}
+            \<^term>\<open>\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)\<close>
+        | Nor => \<^term>\<open>\<lambda> x. \<lambda> y. \<not> (x \<or> y)\<close>
+        | Nand => \<^term>\<open>\<lambda> x. \<lambda> y. \<not> (x \<and> y)\<close>
         | Not => HOLogic.Not
         | Op_Forall => HOLogic.all_const dummyT
         | Op_Exists => HOLogic.exists_const dummyT
-        | True => @{term "True"}
-        | False => @{term "False"}
+        | True => \<^term>\<open>True\<close>
+        | False => \<^term>\<open>False\<close>
         )
    | TypeSymbol _ =>
        raise MISINTERPRET_SYMBOL
         ("Cannot have TypeSymbol in term", symb)
    | System _ =>

   in (mapply args f', thy') end
 
 (*As above, but for products*)
 fun mtimes thy =
   fold (fn x => fn y =>
-    Sign.mk_const thy (@{const_name Pair}, [dummyT, dummyT]) $ y $ x)
+    Sign.mk_const thy (\<^const_name>\<open>Pair\<close>, [dummyT, dummyT]) $ y $ x)
 
 fun mtimes' (args, thy) f =
   let
     val (f', thy') = f thy
   in (mtimes thy' args f', thy') end

     fold (add_interp_symbol_to_thy false) ind_symbols thy
     |> fold (add_interp_symbol_to_thy true) bool_symbols
   end
 
 (*Next batch of functions give info about Isabelle/HOL types*)
-fun is_fun (Type (@{type_name fun}, _)) = true
+fun is_fun (Type (\<^type_name>\<open>fun\<close>, _)) = true
   | is_fun _ = false
-fun is_prod (Type (@{type_name prod}, _)) = true
+fun is_prod (Type (\<^type_name>\<open>prod\<close>, _)) = true
   | is_prod _ = false
-fun dom_type (Type (@{type_name fun}, [ty1, _])) = ty1
+fun dom_type (Type (\<^type_name>\<open>fun\<close>, [ty1, _])) = ty1
 fun is_prod_typed thy config symb =
   let
     fun symb_type const_name =
       Sign.the_const_type thy (full_name thy config const_name)
   in

         val (t_fmla, thy') =
           interpret_formula config language const_map var_types type_map tptp_formula thy
         val ([t1, t2], thy'') =
           fold_map (interpret_term formula_level config language const_map var_types type_map)
            [tptp_t1, tptp_t2] thy'
-      in (mk_n_fun 3 @{const_name If} $ t_fmla $ t1 $ t2, thy'') end
+      in (mk_n_fun 3 \<^const_name>\<open>If\<close> $ t_fmla $ t1 $ t2, thy'') end
   | Term_Num (number_kind, num) =>
       let
         (*FIXME hack*)
         (*
         val tptp_type = case number_kind of

             in ((HOLogic.choice_const dummyT) $ t, thy') end
         | Iota =>
             let val (t, thy') =
               interpret_formula config language const_map var_types type_map
                (Quant (Lambda, bindings, tptp_formula)) thy
-            in (Const (@{const_name The}, dummyT) $ t, thy') end
+            in (Const (\<^const_name>\<open>The\<close>, dummyT) $ t, thy') end
         | Dep_Prod =>
             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
         | Dep_Sum =>
             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
         end

       interpret_file cautious path_prefixes file_name type_map const_map thy
   (*FIXME doesn't check if problem has already been interpreted*)
   in TPTP_Data.map (cons ((prob_name, result))) thy' end
 
 val _ =
-  Outer_Syntax.command @{command_keyword import_tptp} "import TPTP problem"
+  Outer_Syntax.command \<^command_keyword>\<open>import_tptp\<close> "import TPTP problem"
     (Parse.path >> (fn name =>
       Toplevel.theory (fn thy =>
         let val path = Path.explode name
         (*NOTE: assumes include files are located at $TPTP/Axioms
           (which is how TPTP is organised)*)