diff -r fa9e28b23d70 -r 858cab621db2 TFL/rules.ML
--- a/TFL/rules.ML	Thu Aug 25 17:51:11 2005 +0200
+++ b/TFL/rules.ML	Fri Aug 26 08:42:52 2005 +0200
@@ -401,11 +401,11 @@
        val tych = cterm_of sign
        val detype = #t o rep_cterm
        val blist' = map (fn (x,y) => (detype x, detype y)) blist
-       fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
+       fun ?? v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
 
   in
   fold_rev (fn (b as (r1,r2)) => fn thm =>
-        EXISTS(?r2(subst_free[b]
+        EXISTS(?? r2 (subst_free [b]
                    (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
               thm)
        blist' th