src/HOL/Tools/SMT/verit_proof.ML

 
 fun parse_raw_proof_step (p :  SMTLIB.tree) : raw_veriT_node =
   let
     fun rotate_pair (a, (b, c)) = ((a, b), c)
     fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
-      | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
+      | get_id t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
         (SOME (map (fn (SMTLIB.Sym id) => id) source), l)
       | parse_source l = (NONE, l)
     fun parse_subproof rule args id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
         let

 
       (* postprocess conclusion *)
       val new_global_bounds = global_bound_vars_by_rule rule args
       val concl = SMTLIB_Isar.unskolemize_names ctxt concl
 
-      val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
-      val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "cx' =", cx',
+      val _ = (SMT_Config.veriT_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl))
+      val _ = (SMT_Config.veriT_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx',
         "bound_vars =", bound_vars))
       val bound_vars = filter_out (member ((op =)) new_global_bounds) bound_vars
       val bound_tvars =
         map (fn s => (s, the (find_type_in_formula concl s))) bound_vars
       val subproof_cx = add_bound_variables_to_ctxt concl bound_vars cx

   let
     fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems,
         proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, subproof = (_, _, subproof)}) =
       let
         fun mk_prop_of_term concl =
-          concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
+          concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close>
         fun remove_assumption_id assumption_id prems =
           filter_out (curry (op =) assumption_id) prems
         fun inline_assumption assumption assumption_id
             (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt

   end
 
 fun parse_replay typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
-    val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} u)
+    val _ = (SMT_Config.veriT_msg ctxt) (fn () => \<^print> u)
   in
     (u, ctxt_of env)
   end
 end