--- a/src/HOLCF/ex/Loop.ML Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Loop.ML Mon Feb 17 11:04:00 1997 +0100
@@ -57,7 +57,7 @@
(asm_simp_tac HOLCF_ss 1),
(stac while_unfold 1),
(res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
- (etac (flat_tr RS flat_codom RS disjE) 1),
+ (etac (flat_flat RS flat_codom RS disjE) 1),
(atac 1),
(etac spec 1),
(simp_tac HOLCF_ss 1),
@@ -92,7 +92,7 @@
(rtac step_def2 1),
(asm_simp_tac HOLCF_ss 1),
(etac exE 1),
- (etac (flat_tr RS flat_codom RS disjE) 1),
+ (etac (flat_flat RS flat_codom RS disjE) 1),
(asm_simp_tac HOLCF_ss 1),
(asm_simp_tac HOLCF_ss 1)
]);