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;