# HG changeset patch
# User blanchet
# Date 1455536797 -3600
# Node ID 10332fa721b2d224bab9665e1a0025b7640698c3
# Parent  ccb42dbf4aa18a5d89cc65120667f9bdcfa49885
use 'undefined' instead of 'Eps'

diff -r ccb42dbf4aa1 -r 10332fa721b2 src/HOL/Tools/BNF/bnf_comp.ML
--- 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;