TFL/usyntax.ML
changeset 13182 21851696dbf0
parent 12340 24d31d47af1a
child 15531 08c8dad8e399
     1.1 --- a/TFL/usyntax.ML	Mon May 27 17:20:16 2002 +0200
     1.2 +++ b/TFL/usyntax.ML	Tue May 28 09:46:39 2002 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5  fun mk_select (r as {Bvar,Body}) =
     1.6    let val ty = type_of Bvar
     1.7 -      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
     1.8 +      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
     1.9    in list_comb(c,[mk_abs r])
    1.10    end;
    1.11