src/HOL/TPTP/atp_theory_export.ML

     if heading = factsN then (heading, order_facts ord lines) :: problem
     else (heading, lines) :: order_problem_facts ord problem
 
 (* A fairly random selection of types used for monomorphizing. *)
 val ground_types =
-  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
-   @{typ unit}]
+  [\<^typ>\<open>nat\<close>, HOLogic.intT, HOLogic.realT, \<^typ>\<open>nat => bool\<close>, \<^typ>\<open>bool\<close>,
+   \<^typ>\<open>unit\<close>]
 
 fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], [])
   | ground_type_of_tvar thy (T :: Ts) tvar =
     if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
     else ground_type_of_tvar thy Ts tvar
 
 fun monomorphize_term ctxt t =
   let val thy = Proof_Context.theory_of ctxt in
     t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types))
-    handle TYPE _ => @{prop True}
+    handle TYPE _ => \<^prop>\<open>True\<close>
   end
 
 fun heading_sort_key heading =
   if String.isPrefix factsN heading then "_" ^ heading else heading
 

     val problem =
       facts
       |> map (fn ((_, loc), th) =>
         ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
       |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
-        @{prop False}
+        \<^prop>\<open>False\<close>
       |> #1 |> sort_by (heading_sort_key o fst)
     val prelude = fst (split_last problem)
     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
     val infers =
       if infer_policy = No_Inferences then