author | blanchet |
Mon, 15 Feb 2016 12:46:37 +0100 | |
changeset 62316 | 10332fa721b2 |
parent 62315 | ccb42dbf4aa1 |
child 62317 | e1698a9578ea |
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Feb 14 19:44:59 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Feb 15 12:46:37 2016 +0100 @@ -394,7 +394,7 @@ 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;