# HG changeset patch
# User berghofe
# Date 1022571999 -7200
# Node ID 21851696dbf0706a1710d3f134bf636698f86323
# Parent  dc393bbee6cefce5380b8c7f2a007e2daac3c9e2
Eps -> Hilbert_Choice.Eps

diff -r dc393bbee6ce -r 21851696dbf0 TFL/dcterm.ML
--- a/TFL/dcterm.ML	Mon May 27 17:20:16 2002 +0200
+++ b/TFL/dcterm.ML	Tue May 28 09:46:39 2002 +0200
@@ -136,7 +136,7 @@
 val dest_disj   = dest_binop "op |"
 val dest_cons   = dest_binop "Cons"
 val dest_let    = Library.swap o dest_binop "Let";
-val dest_select = dest_binder "Eps"
+val dest_select = dest_binder "Hilbert_Choice.Eps"
 val dest_exists = dest_binder "Ex"
 val dest_forall = dest_binder "All"
 
diff -r dc393bbee6ce -r 21851696dbf0 TFL/usyntax.ML
--- a/TFL/usyntax.ML	Mon May 27 17:20:16 2002 +0200
+++ b/TFL/usyntax.ML	Tue May 28 09:46:39 2002 +0200
@@ -167,7 +167,7 @@
 
 fun mk_select (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
+      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
   in list_comb(c,[mk_abs r])
   end;