--- 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