diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/Tr.ML
--- a/src/HOLCF/Tr.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/Tr.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -157,12 +157,12 @@
    replaced by a more general admissibility test that also checks 
    chain-finiteness, of which these lemmata are specific examples *)
 
-Goal "x~=FF = (x=TT|x=UU)";
+Goal "(x~=FF) = (x=TT|x=UU)";
 by (res_inst_tac [("p","x")] trE 1);
 by (TRYALL (Asm_full_simp_tac));
 qed"adm_trick_1";
 
-Goal "x~=TT = (x=FF|x=UU)";
+Goal "(x~=TT) = (x=FF|x=UU)";
 by (res_inst_tac [("p","x")] trE 1);
 by (TRYALL (Asm_full_simp_tac));
 qed"adm_trick_2";