src/HOL/Tools/ATP/atp_proof_reconstruct.ML

     (case (u, v) of
       (Const (\<^const_name>\<open>True\<close>, _), _) => v
     | (u, Const (\<^const_name>\<open>True\<close>, _)) => u
     | (Const (\<^const_name>\<open>False\<close>, _), v) => s_not v
     | (u, Const (\<^const_name>\<open>False\<close>, _)) => s_not u
-    | _ => if u aconv v then \<^const>\<open>True\<close> else t $ simplify_bool u $ simplify_bool v)
+    | _ => if u aconv v then \<^Const>\<open>True\<close> else t $ simplify_bool u $ simplify_bool v)
   | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
   | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
   | simplify_bool t = t
 
 fun single_letter upper s =

         ATerm ((s, tys), us) =>
         if s = "" (* special marker generated on parse error *) then
           error "Isar proof reconstruction failed because the ATP proof contains unparsable \
             \material"
         else if String.isPrefix native_type_prefix s then
-          \<^const>\<open>True\<close> (* ignore TPTP type information (needed?) *)
+          \<^Const>\<open>True\<close> (* ignore TPTP type information (needed?) *)
         else if s = tptp_equal then
           list_comb (Const (\<^const_name>\<open>HOL.eq\<close>, Type_Infer.anyT \<^sort>\<open>type\<close>),
             map (do_term [] NONE) us)
         else
           (case unprefix_and_unascii const_prefix s of

                   do_term (extra_t :: extra_ts)
                     (case opt_T of SOME T => SOME (slack_fastype_of extra_t --> T) | NONE => NONE)
                     (nth us (length us - 2))
                 end
               else if s' = type_guard_name then
-                \<^const>\<open>True\<close> (* ignore type predicates *)
+                \<^Const>\<open>True\<close> (* ignore type predicates *)
               else
                 let
                   val new_skolem = String.isPrefix new_skolem_const_prefix s''
                   val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
                   val (type_us, term_us) = chop num_ty_args us |>> append mangled_us

     else error "Unsupported Isar reconstruction"
 
 fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
   if String.isPrefix class_prefix s then
     add_type_constraint pos (type_constraint_of_term ctxt u)
-    #> pair \<^const>\<open>True\<close>
+    #> pair \<^Const>\<open>True\<close>
   else
     pair (term_of_atp ctxt format type_enc textual sym_tab (SOME \<^typ>\<open>bool\<close>) u)
 
 (* Update schematic type variables with detected sort constraints. It's not
    totally clear whether this code is necessary. *)

 
 val waldmeister_conjecture_num = "1.0.0.0"
 
 fun repair_waldmeister_endgame proof =
   let
-    fun repair_tail (name, _, \<^const>\<open>Trueprop\<close> $ t, rule, deps) =
-      (name, Negated_Conjecture, \<^const>\<open>Trueprop\<close> $ s_not t, rule, deps)
+    fun repair_tail (name, _, \<^Const>\<open>Trueprop for t\<close>, rule, deps) =
+      (name, Negated_Conjecture, \<^Const>\<open>Trueprop for \<open>s_not t\<close>\<close>, rule, deps)
     fun repair_body [] = []
       | repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
         if num = waldmeister_conjecture_num then map repair_tail (line :: lines)
         else line :: repair_body lines
   in