src/HOLCF/ex/Loop.ML

         (stac step_def2 1),
         (res_inst_tac [("p","b`x")] trE 1),
         (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),
         (asm_simp_tac HOLCF_ss 1),
         (asm_simp_tac HOLCF_ss 1),

         (Simp_tac 1),
         (rtac trans 1),
         (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)
         ]);
 
 val loop_lemma2 = prove_goal Loop.thy