src/HOL/Tools/Metis/metis_tactic.ML

 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Metis_Generate
 open Metis_Reconstruct
 
-val new_skolem = Attrib.setup_config_bool @{binding metis_new_skolem} (K false)
-val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
+val new_skolem = Attrib.setup_config_bool \<^binding>\<open>metis_new_skolem\<close> (K false)
+val advisory_simp = Attrib.setup_config_bool \<^binding>\<open>metis_advisory_simp\<close> (K true)
 
 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
 fun have_common_thm ctxt ths1 ths2 =
   exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
     (map (Meson.make_meta_clause ctxt) ths2)

    "t => t'", where "t" and "t'" are the same term modulo type tags.
    In Isabelle, type tags are stripped away, so we are left with "t = t" or
    "t => t". Type tag idempotence is also handled this way. *)
 fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
   (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
-    Const (@{const_name HOL.eq}, _) $ _ $ t =>
+    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t =>
     let
       val ct = Thm.cterm_of ctxt t
       val cT = Thm.ctyp_of_cterm ct
     in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
-  | Const (@{const_name disj}, _) $ t1 $ t2 =>
+  | Const (\<^const_name>\<open>disj\<close>, _) $ t1 $ t2 =>
     (if can HOLogic.dest_not t1 then t2 else t1)
     |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
   | _ => raise Fail "expected reflexive or trivial clause")
   |> Meson.make_meta_clause ctxt
 

                 Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
                 |> Thm.cterm_of ctxt
                 |> Conv.comb_conv (conv true ctxt))
             else
               Conv.abs_conv (conv false o snd) ctxt ct
-          | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
+          | Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _ => Thm.reflexive ct
           | _ => Conv.comb_conv (conv true ctxt) ct)
       val eq_th = conv true ctxt (Thm.cprop_of th)
       (* We replace the equation's left-hand side with a beta-equivalent term
          so that "Thm.equal_elim" works below. *)
       val t0 $ _ $ t2 = Thm.prop_of eq_th

     fun fall_back () =
       (verbose_warning ctxt
            ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
        FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0)
   in
-    (case filter (fn t => Thm.prop_of t aconv @{prop False}) cls of
+    (case filter (fn t => Thm.prop_of t aconv \<^prop>\<open>False\<close>) cls of
        false_th :: _ => [false_th RS @{thm FalseE}]
      | [] =>
      (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering)
          {axioms = axioms |> map fst, conjecture = []}) of
        Metis_Resolution.Contradiction mth =>

 fun consider_opt s =
   if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
 
 val parse_metis_options =
   Scan.optional
-      (Args.parens (Args.name -- Scan.option (@{keyword ","} |-- Args.name))
+      (Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name))
        >> (fn (s, s') =>
               (NONE, NONE) |> consider_opt s
                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
       (NONE, NONE)
 
 val _ =
   Theory.setup
-    (Method.setup @{binding metis}
+    (Method.setup \<^binding>\<open>metis\<close>
       (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
       "Metis for FOL and HOL problems")
 
 end;