--- a/src/FOL/IFOL.thy Fri Apr 08 23:25:48 2011 +0200 +++ b/src/FOL/IFOL.thy Fri Apr 08 23:33:57 2011 +0200 @@ -590,7 +590,7 @@ use "fologic.ML" -lemma thin_refl: "!!X. [|x=x; PROP W|] ==> PROP W" . +lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" . use "hypsubstdata.ML" setup hypsubst_setup