diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Loop.ML
--- 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)
         ]);