use 'undefined' instead of 'Eps'
authorblanchet
Mon, 15 Feb 2016 12:46:37 +0100
changeset 62316 10332fa721b2
parent 62315 ccb42dbf4aa1
child 62317 e1698a9578ea
use 'undefined' instead of 'Eps'
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;