--- a/src/HOL/UNITY/UNITY.ML Fri May 26 18:06:58 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML Fri May 26 18:07:17 2000 +0200
@@ -55,8 +55,9 @@
qed "surjective_mk_program";
Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
-by (stac (surjective_mk_program RS sym) 1);
-by (stac (surjective_mk_program RS sym) 1 THEN Force_tac 1);
+by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1);
+by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1);
+by (Asm_simp_tac 1);
qed "program_equalityI";
val [major,minor] =