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