--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Jan 05 17:24:33 2019 +0100
@@ -401,7 +401,7 @@
let val (sel_rhs, wits) = mk_sel_case_args lthy ctr_Tss ks arg
in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end;
fun mk_dis_case_args args k = map (fn (k', arg) => (if k = k'
- then fold_rev Term.lambda arg @{const True} else fold_rev Term.lambda arg @{const False})) args;
+ then fold_rev Term.lambda arg \<^const>\<open>True\<close> else fold_rev Term.lambda arg \<^const>\<open>False\<close>)) args;
val sel_rhs = map (map mk_sel_rhs) sel_argss
val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
val dis_qty = qty_isom --> HOLogic.boolT;