src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

 fun curried_type (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>prod\<close>, Ts), T])) =
   Ts ---> T;
 
 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
 
-val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
-val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
+val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>;
+val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>;
 val mk_dnf = mk_disjs o map mk_conjs;
 
-val conjuncts_s = filter_out (curry (op aconv) @{const True}) o HOLogic.conjuncts;
-
-fun s_not @{const True} = @{const False}
-  | s_not @{const False} = @{const True}
-  | s_not (@{const Not} $ t) = t
-  | s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u
-  | s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u
-  | s_not t = @{const Not} $ t;
+val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts;
+
+fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
+  | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
+  | s_not (\<^const>\<open>Not\<close> $ t) = t
+  | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u
+  | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u
+  | s_not t = \<^const>\<open>Not\<close> $ t;
 
 val s_not_conj = conjuncts_s o s_not o mk_conjs;
 
-fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
+fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs;
 fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
 
 fun propagate_units css =
   (case List.partition (can the_single) css of
     ([], _) => css
   | ([u] :: uss, css') =>
     [u] :: propagate_units (map (propagate_unit_neg (s_not u))
       (map (propagate_unit_pos u) (uss @ css'))));
 
 fun s_conjs cs =
-  if member (op aconv) cs @{const False} then @{const False}
-  else mk_conjs (remove (op aconv) @{const True} cs);
+  if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
+  else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs);
 
 fun s_disjs ds =
-  if member (op aconv) ds @{const True} then @{const True}
-  else mk_disjs (remove (op aconv) @{const False} ds);
+  if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
+  else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds);
 
 fun s_dnf css0 =
   let val css = propagate_units css0 in
     if null css then
-      [@{const False}]
+      [\<^const>\<open>False\<close>]
     else if exists null css then
       []
     else
       map (fn c :: cs => (c, cs)) css
       |> AList.coalesce (op =)