src/HOL/Tools/BNF/bnf_lfp_countable.ML

   unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
   ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives);
 
 fun encode_sumN n k t =
   Balanced_Tree.access {init = t,
-      left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
-      right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
+      left = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inl (nat, nat)} $ t),
+      right = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inr (nat, nat)} $ t)}
     n k;
 
 fun encode_tuple [] = \<^term>\<open>0 :: nat\<close>
   | encode_tuple ts =
-    Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+    Balanced_Tree.make (fn (t, u) => \<^const>\<open>prod_encode\<close> $ (@{const Pair (nat, nat)} $ u $ t)) ts;
 
 fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
   let
     val thy = Proof_Context.theory_of ctxt;
 

       |> HOLogic.conj_elims ctxt
       |> Proof_Context.export names_ctxt ctxt
       |> map Thm.close_derivation
     end;
 
-fun get_countable_goal_type_name (@{const Trueprop} $ (Const (\<^const_name>\<open>Ex\<close>, _)
+fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
     $ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0
         $ Const (\<^const_name>\<open>top\<close>, _)))) = s
   | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
 
 fun core_countable_datatype_tac ctxt st =