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