# HG changeset patch
# User wenzelm
# Date 1125237895 -7200
# Node ID 79ab8ea7b097c1a796728722f867385baa54cad8
# Parent  cbe14eb12729233394c9fdfefb5dc172ea614309
avoid symbolic identifier;

diff -r cbe14eb12729 -r 79ab8ea7b097 TFL/rules.ML
--- a/TFL/rules.ML	Sun Aug 28 16:04:54 2005 +0200
+++ b/TFL/rules.ML	Sun Aug 28 16:04:55 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 ex 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(ex r2 (subst_free [b]
                    (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
               thm)
        blist' th