src/HOL/Tools/BNF/bnf_comp.ML

       (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
 
     val ((Asets, lives), _(*names_lthy*)) = lthy
       |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
       ||>> mk_Frees "x" (drop n As);
-    val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
+    val xs = map (fn T => Const (@{const_name undefined}, T)) killedAs @ lives;
 
     val T = mk_T_of_bnf Ds As bnf;
 
     (*bnf.map id ... id*)
     val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);